Tomorrow and All our Yesterdays: MTL Satisfiability over the Integers

DOI10.1007/978-3-540-85762-4_9MaRDI QIDQ5505598zbMATH OpenOpenAlexFDO

Authors Carlo A. Furia, Paola Spoletini

Publication date 27 January 2009

Published in Theoretical Aspects of Computing - ICTAC 2008 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-85762-4_9

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• Some Recent Results in Metric Temporal Logic
• Theorem proving for metric temporal logic over the naturals
• On the Expressiveness of MTL with Past Operators
• On the decidability and complexity of Metric Temporal Logic over finite words
• Making Metric Temporal Logic Rational

Cites work

• scientific article; zbMATH DE number 747023 (Why is no real title available?)
• scientific article; zbMATH DE number 1142314 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 2206109 (Why is no real title available?)
• Model Checking Temporal Metric Specifications with Trio2Promela
• Real-time logics: Complexity and expressiveness
• The complexity of propositional linear temporal logics
• The complexity of propositional linear temporal logics in simple cases

Cited in

(10)

• Satisfiability checking for mission-time \textsf{LTL} (MLTL)
• Theorem proving for metric temporal logic over the naturals
• Checking EMTLK properties of timed interpreted systems via bounded model checking
• Compositional reasoning using intervals and time reversal
• Theorem proving for pointwise metric temporal logic over the naturals via translations
• Temporal Minimal-World Query Answering over Sparse ABoxes
• Combining the temporal and epistemic dimensions for MTL monitoring
• Benchmarking Model- and Satisfiability-Checking on Bi-infinite Time
• SMT-based satisfiability of first-order LTL with event freezing functions and metric operators
• Maximum satisfiability of mission-time linear temporal logic

This page was built for publication: Tomorrow and All our Yesterdays: MTL Satisfiability over the Integers

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