Constraint LTL satisfiability checking without automata
From MaRDI portal
Publication:472802
DOI10.1016/J.JAL.2014.07.005zbMATH Open1310.68141arXiv1205.0946OpenAlexW2162541148MaRDI QIDQ472802FDOQ472802
Publication date: 20 November 2014
Published in: Journal of Applied Logic (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1205.0946
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
Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Cites Work
- A theory of timed automata
- Title not available (Why is that?)
- Completeness of the Bounded Satisfiability Problem for Constraint LTL
- The complexity of propositional linear temporal logics
- A really temporal logic
- Constraint LTL satisfiability checking without automata
- Title not available (Why is that?)
- Linear Encodings of Bounded LTL Model Checking
- Verification, Model Checking, and Abstract Interpretation
- An automata-theoretic approach to constraint LTL
- Title not available (Why is that?)
- Model-checking CTL* over flat Presburger counter systems
- Decidable fragments of first-order temporal logics
- Bounded model checking of infinite state systems
- The effects of bounding syntactic resources on Presburger LTL
- Title not available (Why is that?)
- Title not available (Why is that?)
- Foundations of Software Science and Computation Structures
- CONCUR 2005 – Concurrency Theory
Cited In (10)
- 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
- A logical characterization of timed regular languages
- A tool for deciding the satisfiability of continuous-time metric temporal logic
- Using formal verification to evaluate the execution time of Spark applications
- Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL
- Early verification of legal compliance via bounded satisfiability checking
- SAT-Based Model Checking without Unrolling
Uses Software
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)
