Branching-time model checking of one-counter processes and timed automata

DOI10.1137/120876435MaRDI QIDQ2848205zbMATH OpenOpenAlexFDO

Authors Stefan Göller, Markus Lohrey

Publication date 25 September 2013

Published in SIAM Journal on Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1137/120876435

zbMATH Keywords

timed automataone-counter automatacomputation free logic model checking

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• Branching-time model checking of one-counter processes
• On the complexity of model-checking branching and alternating-time temporal logics in one-counter systems
• Branching-time model checking of parametric one-counter automata
• Model checking succinct and parametric one-counter automata
• CONCUR 2004 - Concurrency Theory

Cited in

(14)

• On the complexity of resource-bounded logics
• Equivalence between model-checking flat counter systems and Presburger arithmetic
• Branching-time model checking of parametric one-counter automata
• Equivalence between model-checking flat counter systems and Presburger arithmetic
• Model Checking Metric Temporal Logic over Automata with One Counter
• Reachability in two-parametric timed automata with one parameter is EXPSPACE-complete
• Branching-time model checking of one-counter processes
• Model Checking FO(R) over One-Counter Processes and beyond
• The complexity of flat freeze LTL
• The complexity of flat freeze LTL
• Computing linear arithmetic representation of reachability relation of one-counter automata
• On the complexity of model-checking branching and alternating-time temporal logics in one-counter systems
• Model checking succinct and parametric one-counter automata
• CONCUR 2004 - Concurrency Theory

This page was built for publication: Branching-time model checking of one-counter processes and timed automata

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