Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Verification of Temporal Properties of Processes in a Setting with Data

Jan Friso Groote5, 6 Contact Information and Radu MateescuContact Information

(5)  Cwi, P.O. Box 94079, NL-1090 GB Amsterdam, The Netherlands
(6)  Eindhoven University of Technology, P.O. Box 513, NL-5600 MB Eindhoven, The Netherlands
(7)  Inria Rhône-Alpes / VASY group, 655, avenue de l’Europe, F-38330 Montbonnot Saint Martin, France
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.
This work has been funded by the grant no. 97-09 of the Ercim fellowship programme for collaboration between Inria and Cwi.

Contact Information Jan Friso Groote
Email: JanFriso.Groote@cwi.nl

Contact Information Radu Mateescu
Email: Radu.Mateescu@inria.fr
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.105 • Server: mpweb17
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)