Linear temporal logic symbolic model checking

DOI10.1016/J.COSREV.2010.06.002zbMATH Open1298.68176OpenAlexW1965024948MaRDI QIDQ465680FDOQ465680

Authors: Kristin Yvonne Rozier 

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

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

zbMATH Keywords

verificationformal methodslinear temporal logic (LTL)symbolic model checking (SMC)

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Cites Work

• NuSMV: A new symbolic model checker
• HyTech: A model checker for hybrid systems
• Computer Aided Verification
• Introduction to algorithms
• Graph-Based Algorithms for Boolean Function Manipulation
• Towards a general theory of action and time
• Symbolic model checking: \(10^{20}\) states and beyond
• Propositional dynamic logic of regular programs
• The complexity of propositional linear temporal logics
• Title not available (Why is that?)
• Title not available (Why is that?)
• Logic in Computer Science
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Title not available (Why is that?)
• Title not available (Why is that?)
• Sanity Checks in Formal Verification
• Enhanced vacuity detection in linear temporal logic.
• Efficient detection of vacuity in temporal model checking
• Title not available (Why is that?)
• Temporal logic can be more expressive
• Title not available (Why is that?)
• Propositional dynamic logic of looping and converse is elementarily decidable
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Decision procedures and expressiveness in the temporal logic of branching time
• “Sometimes” and “not never” revisited
• Decidability of model checking for infinite-state concurrent systems
• Reduction of OBDDs in linear time
• Reasoning about infinite computations
• An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps
• Binary Decision Diagrams
• The Birth of Model Checking
• An automata-theoretic approach to branching-time model checking
• SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Safety, liveness and fairness in temporal logic
• The complementation problem for Büchi automata with applications to temporal logic
• Title not available (Why is that?)
• Deciding full branching time logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Weak alternating automata are not that weak
• Title not available (Why is that?)
• Title not available (Why is that?)
• Defining liveness
• Title not available (Why is that?)
• Proving the Correctness of Multiprocess Programs
• Recognizing safety and liveness
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• ``More deterministic vs. ``smaller Büchi automata for efficient LTL model checking
• Proving Liveness Properties of Concurrent Programs
• Title not available (Why is that?)
• Formal Methods in Computer-Aided Design
• Correct Hardware Design and Verification Methods
• LAR: A logic of algorithmic reasoning
• The nonapproximability of OBDD minimization
• Practical CTL* model checking: Should SPIN be extended?
• Title not available (Why is that?)
• Title not available (Why is that?)
• Liveness checking as safety checking for infinite state spaces
• From Church and Prior to PSL
• Büchi Complementation and Size-Change Termination
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Concepts of Automata Construction from LTL
• From Monadic Logic to PSL
• Automata-Theoretic Model Checking Revisited
• Automated Technology for Verification and Analysis
• Correct Hardware Design and Verification Methods
• Allen Linear (Interval) Temporal Logic – Translation to LTL and Monitor Synthesis
• Improved Algorithms for the Automata-Based Approach to Model-Checking
• Model Checking Software
• A new heuristic for bad cycle detection using BDDs

Cited In (16)

• Optimal control of multi-task Boolean control networks via temporal logic
• Abstraction-based synthesis for stochastic systems with omega-regular objectives
• Linear Temporal Logic of Constraint Automata
• A symbolic model for timed concurrent constraint programming
• Model checking of linear-time properties in multi-valued systems
• The Linear Temporal Logic of Rewriting Maude Model Checker
• BDD-based symbolic model checking
• Title not available (Why is that?)
• Model Checking Software
• Title not available (Why is that?)
• Title not available (Why is that?)
• Towards better heuristics for solving bounded model checking problems
• Applying formal verification to an open-source real-time operating system
• SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
• Model checking properties on reduced trace systems
• The Verus language: Representing time efficiently with BDDs

Uses Software

• SPIN
• HyTech
• NuSMV
• Uppaal
• Java PathFinder
• Cadence SMV
• CESAR
• SPOT
• LTL2BA
• VIS

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)