Constraint LTL satisfiability checking without automata
From MaRDI portal
(Redirected from Publication:472802)
Abstract: This paper introduces a novel technique to decide the satisfiability of formulae written in the language of Linear Temporal Logic with Both future and past operators and atomic formulae belonging to constraint system D (CLTLB(D) for short). The technique is based on the concept of bounded satisfiability, and hinges on an encoding of CLTLB(D) formulae into QF-EUD, the theory of quantifier-free equality and uninterpreted functions combined with D. Similarly to standard LTL, where bounded model-checking and SAT-solvers can be used as an alternative to automata-theoretic approaches to model-checking, our approach allows users to solve the satisfiability problem for CLTLB(D) formulae through SMT-solving techniques, rather than by checking the emptiness of the language of a suitable automaton A_{phi}. The technique is effective, and it has been implemented in our Zot formal verification tool.
Recommendations
- scientific article; zbMATH DE number 1954378
- An automata-theoretic approach to constraint LTL
- \(\mathrm{LTL}_{f}\) satisfiability checking
- SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
- Model checking LTL using constraint programming
- SAT-based explicit LTL reasoning and its application to satisfiability checking
- Completeness of the bounded satisfiability problem for constraint LTL
- Accelerating LTL satisfiability checking by SAT solvers
Cites work
- scientific article; zbMATH DE number 1670482 (Why is no real title available?)
- scientific article; zbMATH DE number 1953038 (Why is no real title available?)
- scientific article; zbMATH DE number 1954378 (Why is no real title available?)
- scientific article; zbMATH DE number 2090318 (Why is no real title available?)
- A really temporal logic
- A theory of timed automata
- An automata-theoretic approach to constraint LTL
- Bounded model checking of infinite state systems
- CONCUR 2005 – Concurrency Theory
- Completeness of the bounded satisfiability problem for constraint LTL
- Constraint LTL satisfiability checking without automata
- Decidable fragments of first-order temporal logics
- Deciding the satisfiability of MITL specifications
- Foundations of Software Science and Computation Structures
- Linear Encodings of Bounded LTL Model Checking
- Model-checking \(\mathrm{CTL}^*\) over flat Presburger counter systems
- The complexity of propositional linear temporal logics
- The effects of bounding syntactic resources on Presburger LTL
- Verification, Model Checking, and Abstract Interpretation
Cited in
(16)- A temporal logic for micro- and macro-step-based real-time systems: foundations and applications
- On the initialization of clocks in timed formalisms
- Constraint LTL satisfiability checking without automata
- An SMT-based approach to satisfiability checking of MITL
- Trace-length independent runtime monitoring of quantitative policies in LTL
- A logical characterization of timed regular languages
- Accelerating LTL satisfiability checking by SAT solvers
- Completeness of the bounded satisfiability problem for constraint LTL
- Variable and clause elimination for LTL satisfiability checking
- A tool for deciding the satisfiability of continuous-time metric temporal logic
- Using formal verification to evaluate the execution time of Spark applications
- SMT-based satisfiability of first-order LTL with event freezing functions and metric operators
- \(\mathrm{LTL}_{f}\) satisfiability checking
- SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
- SAT-Based Model Checking without Unrolling
- Early verification of legal compliance via bounded satisfiability checking
This page was built for publication: Constraint LTL satisfiability checking without automata
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q472802)
