Verification of temporal properties of processes in a setting with data

DOI10.1007/3-540-49253-4_8MaRDI QIDQ4250361zbMATH OpenFDO

Authors Jan Friso Groote, Radu Mateescu

Publication date 17 June 1999

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://ir.cwi.nl/pub/1904

zbMATH Keywords

fixed point operatorsmodal \(\mu\)-calculusprocess algebra

Mathematics Subject Classification ID

Temporal logic (03B44) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Model-checking processes with data
• scientific article; zbMATH DE number 2087443
• Local model checking for value-passing processes. (Extended abstract)
• scientific article; zbMATH DE number 1231562

Cited in

(19)

• Model-checking processes with data
• Parameterised Boolean equation systems
• Tableaux for verification of data-centric processes
• Suitability of mCRL2 for concurrent-system design: a 2 2 Switch case study
• Model Checking Value-Passing Modal Specifications
• scientific article; zbMATH DE number 2087443 (Why is no real title available?)
• scientific article; zbMATH DE number 7136664 (Why is no real title available?)
• scientific article; zbMATH DE number 7269247 (Why is no real title available?)
• Abstraction in fixpoint logic
• A linear translation from CTL^* to the first-order modal -calculus
• Instantiation for Parameterised Boolean Equation Systems
• Towards automatic temporal logic verification of value passing process algebra using abstract interpretation
• Operations on fixpoint equation systems
• Constraint automata on infinite data trees: from \(\mathrm{CTL}(\mathbb{Z})/\mathrm{CTL}^*(\mathbb{Z})\) to decision procedures
• Constraint automata on infinite data trees: from CTL\((\mathbb{Z})\text{CTL}^*(\mathbb{Z})\) to decision procedures
• Verification of reactive systems via instantiation of parameterised Boolean equation systems
• Monitorability for the modal -calculus over systems with data: from practice to theory
• A linear process-algebraic format with data for probabilistic automata
• Invariants for parameterised Boolean equation systems

This page was built for publication: Verification of temporal properties of processes in a setting with data

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4250361)