MTL and TPTL for One-Counter Machines

DOI10.1145/3372789zbMATH Open1433.68215OpenAlexW2995528133WikidataQ130896556 ScholiaQ130896556MaRDI QIDQ5216144FDOQ5216144

Claudia Carapelle, Shiguang Feng, Karin Quaas, Oliver Fernández Gil

Publication date: 14 February 2020

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/3372789

Recommendations

• Model checking succinct and parametric one-counter automata
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Model Checking Metric Temporal Logic over Automata with One Counter
• Model checking memoryful linear-time logics over one-counter automata
• On the complexity of model-checking branching and alternating-time temporal logics in one-counter systems
• DP lower bounds for equivalence-checking and model-checking of one-counter automata
• MTL-model checking of one-clock parametric timed automata is undecidable
• One-counter verifiers for decidable languages
• Model Checking FO(R) over One-Counter Processes and beyond
• Towards certified model checking for PLTL using one-pass tableaux

zbMATH Keywords

metric temporal logicdata wordsone-counter machinesEhrenfeucht-Fraïssé gamesFreeze LTLtimed propositional temporal logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44)

Cited In (2)

• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Generalizing Non-punctuality for Timed Temporal Logic with Freeze Quantifiers

This page was built for publication: MTL and TPTL for One-Counter Machines

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