Selective mu-calculus and formula-based equivalence of transition systems

DOI10.1006/JCSS.1999.1660zbMath0958.68122OpenAlexW2063176706MaRDI QIDQ1970206

Roberto Barbuti, Nicoletta De Francesco, Gigliola Vaglini, Antonella Santone

Publication date: 19 March 2000

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/cf5b35ab2de9bed2ad35f16e9dcd54366737d4eb

zbMATH Keywords

labeled transition systemselective mu-calculus

Mathematics Subject Classification ID

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

Related Items (12)

Abstracting Models from Execution Traces for Performing Formal Verification ⋮ \(\text{DELFIN}^+\): an efficient deadlock detection tool for CCS processes ⋮ Cartesian difference categories ⋮ Model checking properties on reduced trace systems ⋮ A FORMULA-DRIVEN MODULAR ATTACK ON STATE EXPLOSION ⋮ Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities ⋮ Formal Verification of Concurrent Systems via Directed Model Checking ⋮ A local approach for temporal model checking of Java bytecode ⋮ Abstract reduction in directed model checking CCS processes ⋮ Using heuristic search for finding deadlocks in concurrent systems ⋮ Compositional verification of asynchronous concurrent systems using CADP ⋮ Reduced models for efficient CCS verification

Uses Software

• LOTOS
• CADP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Results on the propositional \(\mu\)-calculus
• Tableau-based model checking in the propositional mu-calculus
• Local model checking for infinite state spaces
• Compositionality in state space verification methods

This page was built for publication: Selective mu-calculus and formula-based equivalence of transition systems