Tomorrow and All our Yesterdays: MTL Satisfiability over the Integers

DOI10.1007/978-3-540-85762-4_9zbMATH Open1161.68567OpenAlexW1581639155MaRDI QIDQ5505598FDOQ5505598

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

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

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)

Cites Work

• The complexity of propositional linear temporal logics in simple cases
• Model Checking Temporal Metric Specifications with Trio2Promela
• The complexity of propositional linear temporal logics
• Title not available (Why is that?)
• Title not available (Why is that?)
• Real-time logics: Complexity and expressiveness
• Title not available (Why is that?)
• Title not available (Why is that?)

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)