Theorem proving for pointwise metric temporal logic over the naturals via translations

DOI10.1007/s10817-020-09541-4zbMath1459.03012OpenAlexW3008764564MaRDI QIDQ2228435

Ana Ozaki, Clare Dixon, Ullrich Hustadt

Publication date: 17 February 2021

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-020-09541-4

zbMATH Keywords

modellingschedulingtheorem provingtraffic managementroboticsmetric temporal logic

Mathematics Subject Classification ID

Deterministic scheduling theory in operations research (90B35) Logic in computer science (03B70) Traffic problems in operations research (90B20) Mechanization of proofs and logical operations (03B35) Temporal logic (03B44) Artificial intelligence for robotics (68T40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• NuSMV
• TSPASS
• TRP++
• GitHub
• Aalta
• Leviathan

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A tool for deciding the satisfiability of continuous-time metric temporal logic
• Model-checking in dense real-time
• Real-time logics: Complexity and expressiveness
• Robustness of temporal logic specifications for continuous-time signals
• Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners
• An integrated approach for modeling and solving the general multiprocessor job-shop scheduling problem using tabu search
• Metric temporal description logics with interval-rigid names
• Theorem proving for metric temporal logic over the naturals
• A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance
• And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL
• Temporal Logic with Capacity Constraints
• Some Recent Results in Metric Temporal Logic
• Implementing a fair monodic temporal logic prover
• The complexity of propositional linear temporal logics
• A really temporal logic
• A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution
• The benefits of relaxing punctuality
• On metric temporal description logics
• Querying Log Data with Metric Temporal Logic
• A resolution calculus for the branching-time temporal logic CTL
• Bounds for Certain Multiprocessing Anomalies