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

DOI10.1016/J.IC.2022.104923MaRDI QIDQ2105410zbMATH OpenOpenAlexFDO

Authors Jianwen Li, Moshe Y. Vardi, 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

conflict-driven satisfiability checkingLTL over finite tracesSAT-based satisfiability checkingsatisfiability checking

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Recommendations

• Satisfiability checking for mission-time LTL
• Maximum satisfiability of mission-time linear temporal logic
• An SMT-based approach to satisfiability checking of MITL
• A tool for deciding the satisfiability of continuous-time metric temporal logic
• Tomorrow and All our Yesterdays: MTL Satisfiability over the Integers

Cites work

• A really temporal logic
• An SMT-based approach to satisfiability checking of MITL
• Enhanced vacuity detection in linear temporal logic.
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• More scalable LTL model checking via discovering design-space dependencies \((D^3)\)
• Some Recent Results in Metric Temporal Logic
• Synthesizing non-vacuous systems
• The benefits of relaxing punctuality
• The complexity of propositional linear temporal logics
• The unary fragments of metric interval temporal logic: bounded versus lower bound constraints
• Theorem proving for metric temporal logic over the naturals
• Tomorrow and All our Yesterdays: MTL Satisfiability over the Integers

Cited in

(4)

• Satisfiability checking for mission-time LTL
• Synchronous or alternating? LTL black-box checking of Mealy machines by combining the LearnLib and LTSmin
• Early verification of legal compliance via bounded satisfiability checking
• Maximum satisfiability of mission-time linear temporal logic

Describes a project that uses

Uses Software

• nuXmv
• z3

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2105410)