Model Checking FO(R) over One-Counter Processes and beyond

DOI10.1007/978-3-642-04027-6_35zbMath1257.68106OpenAlexW1487351738MaRDI QIDQ3644768

Anthony Widjaja To

Publication date: 12 November 2009

Published in: Computer Science Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-04027-6_35

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Bisimulation equivalence and regularity for real-time one-counter automata

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algorithmic uses of the Feferman-Vaught theorem
• A uniform method for proving lower bounds on the computational complexity of logical theories
• The theory of ends, pushdown automata, and second-order logic
• The complexity of optimization problems
• Logically defined subsets of \(\mathbb{N}{}^ k\)
• The computational complexity of logical theories
• Pushdown processes: Games and model-checking
• Model checking LTL with regular valuations for pushdown systems
• DP lower bounds for equivalence-checking and model-checking of one-counter automata
• A note on emptiness for alternating finite automata with a one-letter alphabet
• Reachability problems on regular ground tree rewriting graphs
• Theory of computation.
• First-order logic with two variables and unary temporal logic
• Symbolic Model Checking of Tense Logics on Rational Kripke Models
• On compositionality and its limitations
• The succinctness of first-order logic on linear orders
• Mathematical Foundations of Computer Science 2003
• Model Checking Synchronized Products of Infinite Transition Systems
• Recurrent Reachability Analysis in Regular Model Checking
• Foundations of Software Science and Computation Structures
• Decidability of model checking with the temporal logic EF