Satisfiability checking for mission-time \textsf{LTL} (MLTL)

DOI10.1016/j.ic.2022.104923OpenAlexW4281812495MaRDI QIDQ2105410

Moshe Y. Vardi, Jianwen Li, Kristin Yvonne Rozier

Publication date: 8 December 2022

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2022.104923

zbMATH Keywords

satisfiability checkingconflict-driven satisfiability checkingLTL over finite tracesSAT-based satisfiability checking

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Uses Software

• z3
• nuXmv

Cites Work

• An SMT-based approach to satisfiability checking of MITL
• More scalable LTL model checking via discovering design-space dependencies \((D^3)\)
• Theorem proving for metric temporal logic over the naturals
• Synthesizing Non-Vacuous Systems
• Some Recent Results in Metric Temporal Logic
• The complexity of propositional linear temporal logics
• A really temporal logic
• The benefits of relaxing punctuality
• The Unary Fragments of Metric Interval Temporal Logic: Bounded versus Lower Bound Constraints
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Tomorrow and All our Yesterdays: MTL Satisfiability over the Integers
• Computer Aided Verification

This page was built for publication: Satisfiability checking for mission-time \textsf{LTL} (MLTL)