Verification of temporal properies of processes in a setting with data

J.F. Groote, R. Mateescu

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

41 Citaten (Scopus)


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.
Originele taal-2Engels
TitelAlgebraic Methodology and Software Technology (Proceedings 7th International Conference, AMAST'98, Amazonia, Brasil, January 408, 1999)
RedacteurenA.M. Haeberer
Plaats van productieBerlin
ISBN van geprinte versie3-540-65462-3
StatusGepubliceerd - 1999

Publicatie series

NaamLecture Notes in Computer Science
ISSN van geprinte versie0302-9743

Citeer dit