Linear temporal logic symbolic model checking
From MaRDI portal
Publication:465680
DOI10.1016/j.cosrev.2010.06.002zbMath1298.68176OpenAlexW1965024948MaRDI QIDQ465680
Publication date: 24 October 2014
Published in: Computer Science Review (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.cosrev.2010.06.002
Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Temporal logic (03B44)
Related Items (8)
BDD-Based Symbolic Model Checking ⋮ Abstraction-based synthesis for stochastic systems with omega-regular objectives ⋮ Towards better heuristics for solving bounded model checking problems ⋮ Model checking properties on reduced trace systems ⋮ Optimal control of multi-task Boolean control networks via temporal logic ⋮ A symbolic model for timed concurrent constraint programming ⋮ Model checking of linear-time properties in multi-valued systems ⋮ SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
Uses Software
Cites Work
- Towards a general theory of action and time
- Defining liveness
- The complementation problem for Büchi automata with applications to temporal logic
- Recognizing safety and liveness
- Symbolic model checking: \(10^{20}\) states and beyond
- LAR: A logic of algorithmic reasoning
- Propositional dynamic logic of regular programs
- Reduction of OBDDs in linear time
- Reasoning about infinite computations
- Safety, liveness and fairness in temporal logic
- The nonapproximability of OBDD minimization
- Practical CTL* model checking: Should SPIN be extended?
- NuSMV: A new symbolic model checker
- HyTech: A model checker for hybrid systems
- Decidability of model checking for infinite-state concurrent systems
- Decision procedures and expressiveness in the temporal logic of branching time
- An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps
- Temporal logic can be more expressive
- The Birth of Model Checking
- From Church and Prior to PSL
- SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR
- Weak alternating automata are not that weak
- Büchi Complementation and Size-Change Termination
- Propositional dynamic logic of looping and converse is elementarily decidable
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Deciding full branching time logic
- Graph-Based Algorithms for Boolean Function Manipulation
- “Sometimes” and “not never” revisited
- The complexity of propositional linear temporal logics
- Proving Liveness Properties of Concurrent Programs
- Proving the Correctness of Multiprocess Programs
- Binary Decision Diagrams
- Logic in Computer Science
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- Computer Aided Verification
- An automata-theoretic approach to branching-time model checking
- Concepts of Automata Construction from LTL
- From Monadic Logic to PSL
- Automata-Theoretic Model Checking Revisited
- Automated Technology for Verification and Analysis
- Formal Methods in Computer-Aided Design
- Correct Hardware Design and Verification Methods
- Correct Hardware Design and Verification Methods
- Sanity Checks in Formal Verification
- Allen Linear (Interval) Temporal Logic – Translation to LTL and Monitor Synthesis
- Improved Algorithms for the Automata-Based Approach to Model-Checking
- Correct Hardware Design and Verification Methods
- Model Checking Software
- Computer Aided Verification
- A new heuristic for bad cycle detection using BDDs
- Efficient detection of vacuity in temporal model checking
- 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
- 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: Linear temporal logic symbolic model checking
