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

DOI10.1007/S10817-020-09541-4MaRDI QIDQ2228435zbMATH OpenOpenAlexFDO

Authors Ullrich Hustadt, Ana Ozaki, Clare Dixon

Publication date 17 February 2021

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

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

metric temporal logicmodellingroboticsschedulingtheorem provingtraffic management

Mathematics Subject Classification ID

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

Recommendations

• Theorem proving for metric temporal logic over the naturals
• Some Recent Results in Metric Temporal Logic
• Making Metric Temporal Logic Rational
• Tomorrow and All our Yesterdays: MTL Satisfiability over the Integers
• scientific article; zbMATH DE number 7056237

Cites work

• A new rule for LTL tableaux
• A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution
• A PLTL-prover based on labelled superposition with partial model guidance
• A really temporal logic
• A resolution calculus for the branching-time temporal logic CTL
• A tool for deciding the satisfiability of continuous-time metric temporal logic
• An integrated approach for modeling and solving the general multiprocessor job-shop scheduling problem using tabu search
• And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL
• Bounds for Certain Multiprocessing Anomalies
• Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners
• scientific article; zbMATH DE number 1189110 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• Implementing a fair monodic temporal logic prover
• Metric temporal description logics with interval-rigid names
• Model-checking in dense real-time
• On metric temporal description logics
• Querying log data with metric temporal logic
• Real-time logics: Complexity and expressiveness
• Robustness of temporal logic specifications for continuous-time signals
• Some Recent Results in Metric Temporal Logic
• Temporal Logic with Capacity Constraints
• The benefits of relaxing punctuality
• The complexity of propositional linear temporal logics
• Theorem proving for metric temporal logic over the naturals

Cited in

(3)

• Theorem proving for metric temporal logic over the naturals
• Maximum satisfiability of mission-time linear temporal logic
• Complexity of metric temporal logics with counting and the Pnueli modalities

Describes a project that uses

Uses Software

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

This page was built for publication: Theorem proving for pointwise metric temporal logic over the naturals via translations

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