Verification of temporal properies of processes in a setting with data

J.F. Groote, R. Mateescu

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

38 Citations (Scopus)

Abstract

We define a value-based modal µ-calculus, built from firstorder formulas, modalities, and fixed point operators parameterized by data variables, which allows to express temporal properties involving data. We interpret this logic over µCrl terms defined by linear process equations. The satisfaction of a temporal formula by a µCrl term is translated to the satisfaction of a first-order formula containing parameterized fixed point operators. We provide proof rules for these fixed point operators and show their applicability on various examples.
Original languageEnglish
Title of host publicationAlgebraic Methodology and Software Technology (Proceedings 7th International Conference, AMAST'98, Amazonia, Brasil, January 408, 1999)
EditorsA.M. Haeberer
Place of PublicationBerlin
PublisherSpringer
Pages74-90
ISBN (Print)3-540-65462-3
DOIs
Publication statusPublished - 1999

Publication series

NameLecture Notes in Computer Science
Volume1548
ISSN (Print)0302-9743

Cite this

Groote, J. F., & Mateescu, R. (1999). Verification of temporal properies of processes in a setting with data. In A. M. Haeberer (Ed.), Algebraic Methodology and Software Technology (Proceedings 7th International Conference, AMAST'98, Amazonia, Brasil, January 408, 1999) (pp. 74-90). (Lecture Notes in Computer Science; Vol. 1548). Springer. https://doi.org/10.1007/3-540-49253-4_8