Model checking succinct and parametric one-counter automata

DOI10.1007/978-3-642-14162-1_48MaRDI QIDQ3587469zbMATH OpenOpenAlexFDO

Authors Stefan Göller, Christoph Haase, Joël Ouaknine, James Worrell

Publication date 7 September 2010

Published in Automata, Languages and Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14162-1_48

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Reachability in Succinct and Parametric One-Counter Automata
• Branching-time model checking of parametric one-counter automata
• Model checking memoryful linear-time logics over one-counter automata
• Model Checking Metric Temporal Logic over Automata with One Counter
• Branching-time model checking of one-counter processes and timed automata

Cited in

(22)

• One-counter automata for parsing and language approximation
• Synthesis problems for one-counter automata
• Reachability games with relaxed energy constraints
• Branching-time model checking of one-counter processes and timed automata
• Branching-time model checking of parametric one-counter automata
• A Succinct Canonical Register Automaton Model
• Reachability in Succinct and Parametric One-Counter Automata
• On the complexity of model-checking branching and alternating-time temporal logics in one-counter systems
• A succinct canonical register automaton model
• Model Checking Metric Temporal Logic over Automata with One Counter
• The complexity of flat freeze LTL
• Reachability games with relaxed energy constraints
• scientific article; zbMATH DE number 7559494 (Why is no real title available?)
• The complexity of flat freeze LTL
• On parametric timed automata and one-counter machines
• MTL and TPTL for One-Counter Machines
• Countdown games, and simulation on (succinct) one-counter nets
• Reachability in two-parametric timed automata with one parameter is EXPSPACE-complete
• Invariants for one-counter automata with disequality tests
• Parikh one-counter automata
• Reachability in two-parametric timed automata with one parameter is expspace-complete
• Model checking memoryful linear-time logics over one-counter automata

This page was built for publication: Model checking succinct and parametric one-counter automata

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