Stepwise CTL model checking of state/event systems

DOI10.1007/3-540-48683-6_28MaRDI QIDQ4818799zbMATH OpenFDO

Authors Jørn Lind-Nielsen, Henrik Reif Andersen

Publication date 24 September 2004

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

Full work available at URL https://doi.org/10.1007/3-540-48683-6_28

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)

Recommendations

• Structural symbolic CTL model checking of asynchronous systems.
• Symbolic model checking: \(10^{20}\) states and beyond
• Symbolic model checking with fewer fixpoint computations
• Verification of large state/event systems using compositionality and dependency analysis
• scientific article; zbMATH DE number 910719

Cited in

(10)

• Compositional abstraction refinement for control synthesis
• A framework for compositional verification of multi-valued systems via abstraction-refinement
• Stepwise refinement and concurrency: The finite-state case
• CTL-property transformations along an incremental design process
• STP Approach to Model Controlled Automata with Application to Reachability Analysis of DEDS
• Model Checking CTL is Almost Always Inherently Sequential
• Structural symbolic CTL model checking of asynchronous systems.
• Integrated Formal Methods
• Verification of large state/event systems using compositionality and dependency analysis
• Taking Some Burden Off an Explicit CTL Model Checker

Describes a project that uses

Uses Software

• CUDD
• visualSTATE

This page was built for publication: Stepwise CTL model checking of state/event systems

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