Towards the hierarchical verification of reactive systems

DOI10.1016/J.TCS.2003.08.009zbMath1071.68061OpenAlexW2046950395MaRDI QIDQ596025

Frank Salger, Mila E. Majster-Cederbaum

Publication date: 10 August 2004

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2003.08.009

zbMATH Keywords

VerificationModal mu-calculusReactive systemsSyntactic action refinement

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (3)

Towards the hierarchical verification of reactive systems ⋮ On hierarchically developing reactive systems ⋮ Connection between logical and algebraic approaches to concurrent systems

Cites Work

• Towards the hierarchical verification of reactive systems
• Results on the propositional \(\mu\)-calculus
• Local model checking in the modal mu-calculus
• Local model checking for infinite state spaces
• The connection between an event structure semantics and an operational semantics for TCSP
• CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
• Property preserving abstractions for the verification of concurrent systems
• Extension of synthesis algorithm of recursive processes to \(\mu\)-calculus
• An improved algorithm for the evaluation of fixpoint expressions
• Vertical implementation
• Comparing syntactic and semantic action refinement
• Model checking the full modal mu-calculus for infinite sequential processes
• A lattice-theoretical fixpoint theorem and its applications
• Graph-Based Algorithms for Boolean Function Manipulation
• Three Partition Refinement Algorithms
• Abstract Interpretation Frameworks
• Action refinement and property inheritance in systems of sequential agents
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Towards the hierarchical verification of reactive systems