MTL and TPTL for One-Counter Machines

DOI10.1145/3372789MaRDI QIDQ5216144zbMATHOpenAlexWikidataFDO

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

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

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)

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

Cited in

(5)

• Satisfiability for MTL and TPTL over non-monotonic data words
• Generalizing Non-punctuality for Timed Temporal Logic with Freeze Quantifiers
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• On expressive powers of timed logics: comparing boundedness, non-punctuality, and deterministic freezing
• Foundations of Software Science and Computation Structures

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)