Linear temporal logic symbolic model checking
From MaRDI portal
Recommendations
- Model checking general linear temporal logic
- A model checker for linear time temporal logic
- Symbolic model checking for alternating projection temporal logic
- Model-checking timed temporal logics
- Symbolic model checking for temporal-epistemic logic
- A symbolic model checker for propositional projection temporal logic
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- scientific article; zbMATH DE number 1701759
- Linear parametric model checking of timed automata
- Model checking linear coalgebraic temporal logics: an automata-theoretic approach
Cites work
- scientific article; zbMATH DE number 1633145 (Why is no real title available?)
- scientific article; zbMATH DE number 1670767 (Why is no real title available?)
- scientific article; zbMATH DE number 1670781 (Why is no real title available?)
- scientific article; zbMATH DE number 1705164 (Why is no real title available?)
- scientific article; zbMATH DE number 1705167 (Why is no real title available?)
- scientific article; zbMATH DE number 3870578 (Why is no real title available?)
- scientific article; zbMATH DE number 3922633 (Why is no real title available?)
- scientific article; zbMATH DE number 43591 (Why is no real title available?)
- scientific article; zbMATH DE number 177511 (Why is no real title available?)
- scientific article; zbMATH DE number 3469999 (Why is no real title available?)
- scientific article; zbMATH DE number 3594626 (Why is no real title available?)
- scientific article; zbMATH DE number 1069483 (Why is no real title available?)
- scientific article; zbMATH DE number 1142326 (Why is no real title available?)
- scientific article; zbMATH DE number 1973991 (Why is no real title available?)
- scientific article; zbMATH DE number 2080056 (Why is no real title available?)
- scientific article; zbMATH DE number 1487477 (Why is no real title available?)
- scientific article; zbMATH DE number 1744958 (Why is no real title available?)
- scientific article; zbMATH DE number 1796123 (Why is no real title available?)
- scientific article; zbMATH DE number 1796144 (Why is no real title available?)
- scientific article; zbMATH DE number 1903365 (Why is no real title available?)
- scientific article; zbMATH DE number 1903373 (Why is no real title available?)
- scientific article; zbMATH DE number 2102704 (Why is no real title available?)
- scientific article; zbMATH DE number 2102710 (Why is no real title available?)
- scientific article; zbMATH DE number 1392300 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- scientific article; zbMATH DE number 3237829 (Why is no real title available?)
- scientific article; zbMATH DE number 3353170 (Why is no real title available?)
- A new heuristic for bad cycle detection using BDDs
- Allen Linear (Interval) Temporal Logic – Translation to LTL and Monitor Synthesis
- An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps
- An automata-theoretic approach to branching-time model checking
- Automata-Theoretic Model Checking Revisited
- Automated Technology for Verification and Analysis
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Binary Decision Diagrams
- Büchi Complementation and Size-Change Termination
- Computer Aided Verification
- Computer Aided Verification
- Concepts of Automata Construction from LTL
- Correct Hardware Design and Verification Methods
- Correct Hardware Design and Verification Methods
- Decidability of model checking for infinite-state concurrent systems
- Deciding full branching time logic
- Decision procedures and expressiveness in the temporal logic of branching time
- Defining liveness
- Efficient detection of vacuity in temporal model checking
- Enhanced vacuity detection in linear temporal logic.
- Formal Methods in Computer-Aided Design
- From Church and Prior to PSL
- From Monadic Logic to PSL
- Graph-Based Algorithms for Boolean Function Manipulation
- HyTech: A model checker for hybrid systems
- Improved Algorithms for the Automata-Based Approach to Model-Checking
- Introduction to algorithms
- LAR: A logic of algorithmic reasoning
- Liveness checking as safety checking for infinite state spaces
- Logic in Computer Science
- Model Checking Software
- NuSMV: A new symbolic model checker
- Practical CTL* model checking: Should SPIN be extended?
- Propositional dynamic logic of looping and converse is elementarily decidable
- Propositional dynamic logic of regular programs
- Proving Liveness Properties of Concurrent Programs
- Proving the Correctness of Multiprocess Programs
- Reasoning about infinite computations
- Recognizing safety and liveness
- Reduction of OBDDs in linear time
- SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR
- Safety, liveness and fairness in temporal logic
- Sanity Checks in Formal Verification
- Symbolic model checking: \(10^{20}\) states and beyond
- Temporal logic can be more expressive
- The Birth of Model Checking
- The complementation problem for Büchi automata with applications to temporal logic
- The complexity of propositional linear temporal logics
- The nonapproximability of OBDD minimization
- Tools and Algorithms for the Construction and Analysis of Systems
- Towards a general theory of action and time
- Weak alternating automata are not that weak
- ``More deterministic vs. ``smaller Büchi automata for efficient LTL model checking
- “Sometimes” and “not never” revisited
Cited in
(16)- Optimal control of multi-task Boolean control networks via temporal logic
- Abstraction-based synthesis for stochastic systems with omega-regular objectives
- A symbolic model for timed concurrent constraint programming
- Linear Temporal Logic of Constraint Automata
- Model checking of linear-time properties in multi-valued systems
- The Linear Temporal Logic of Rewriting Maude Model Checker
- BDD-based symbolic model checking
- scientific article; zbMATH DE number 1630128 (Why is no real title available?)
- Model Checking Software
- scientific article; zbMATH DE number 6454071 (Why is no real title available?)
- scientific article; zbMATH DE number 1982196 (Why is no real title available?)
- Towards better heuristics for solving bounded model checking problems
- Model checking properties on reduced trace systems
- SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
- Applying formal verification to an open-source real-time operating system
- The Verus language: Representing time efficiently with BDDs
Describes a project that uses
Uses Software
This page was built for publication: Linear temporal logic symbolic model checking
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q465680)
