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

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

Ullrich Hustadt, Clare Dixon, Ana Ozaki

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

modelling; scheduling; theorem proving; traffic management; robotics; metric temporal logic

Mathematics Subject Classification ID

90B35: Deterministic scheduling theory in operations research

03B70: Logic in computer science

90B20: Traffic problems in operations research

03B35: Mechanization of proofs and logical operations

03B44: Temporal logic

68T40: Artificial intelligence for robotics

68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Uses Software

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