Reasoning about reversal-bounded counter machines
From MaRDI portal
Publication:6599624
DOI10.1007/978-3-319-97879-6_17zbMATH Open1544.03031MaRDI QIDQ6599624
Publication date: 6 September 2024
Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) First-order arithmetic and fragments (03F30) Temporal logic (03B44) Classical models of computation (Turing machines, etc.) (68Q04)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Recursive unsolvability of Post's problem of Tag und other topics in theory of Turing machines
- Decidability of a temporal logic problem for Petri nets
- DAL -- a logic for data analysis
- Logic of nondeterministic information
- An analysis of the nonemptiness problem for classes of reversal-bounded multicounter machines
- Problems concerning fairness and temporal logic for conflict-free Petri nets
- The complexity of logical theories
- A note on semilinear sets and bounded-reversal multihead pushdown automata
- Reversal-bounded multipushdown machines
- The covering and boundedness problems for vector addition systems
- Well-abstracted transition systems: Application to FIFO automata.
- Corrigendum to: ``DAL -- a logic for data analysis
- Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt.
- Counter machines and verification problems.
- Presburger liveness verification of discrete timed automata.
- Taming past LTL and flat counter systems
- Semigroups, Presburger formulas, and languages
- Relationships between nondeterministic and deterministic tape complexities
- Parallel program schemata
- Temporal Logics in Computer Science
- Reasoning about Data Repetitions with Counter Systems
- Global Model Checking of Ordered Multi-Pushdown Systems
- The Complexity of Reversal-Bounded Model-Checking
- Integer Vector Addition Systems with States
- Logic For Reasoning About Knowledge
- When Model-Checking Freeze LTL over Counter Machines Becomes Decidable
- Fast Acceleration of Ultimately Periodic Relations
- Reversal-Bounded Counter Machines Revisited
- Relational dual tableaux for interval temporal logics ★
- Linear-time temporal logics with Presburger constraints: an overview ★
- An Algorithm for the General Petri Net Reachability Problem
- Verification Decidability of Presburger Array Programs
- On the complexity of integer programming
- Bounds on Positive Integral Solutions of Linear Diophantine Equations
- Reversal-Bounded Multicounter Machines and Their Decision Problems
- Dynamic logic with program specifications and its relational proof system
- A hierarchy of modal logics with relative accessibility relations
- Deciding properties of integral relational automata
- Subclasses of presburger arithmetic and the weak EXP hierarchy
- Demystifying Reachability in Vector Addition Systems
- On the Complexity of Verifying Regular Properties on Flat Counter Systems,
- Complexity of pattern-based verification for multithreaded programs
- On Context-Free Languages
- Tools and Algorithms for the Construction and Analysis of Systems
- Reachability Problem for Weak Multi-Pushdown Automata
- Proving safety properties of infinite state systems by compilation into Presburger arithmetic
- On the complexity of the linear-time μ-calculus for Petri Nets
This page was built for publication: Reasoning about reversal-bounded counter machines
