Equivalence between model-checking flat counter systems and Presburger arithmetic (Q2636509): Difference between revisions

@@ Property / author @@
-Stéphane P. Demri
@@ Property / author: Stéphane P. Demri / rank @@
-Normal rank
@@ Property / author @@
+Stéphane P. Demri
@@ Property / author: Stéphane P. Demri / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+z3
@@ Property / describes a project that uses: z3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CVC4
@@ Property / describes a project that uses: CVC4 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+TaPAS
@@ Property / describes a project that uses: TaPAS / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.tcs.2017.07.007
+Normal rank
@@ Property / OpenAlex ID @@
+W2737769985
@@ Property / OpenAlex ID: W2737769985 / rank @@
+Normal rank
@@ Property / cites work @@
+The complexity of logical theories
@@ Property / cites work: The complexity of logical theories / rank @@
+Normal rank
@@ Property / cites work @@
+The Complexity of Reversal-Bounded Model-Checking
@@ Property / cites work: The Complexity of Reversal-Bounded Model-Checking / rank @@
+Normal rank
@@ Property / cites work @@
+Safety Problems Are NP-complete for Flat Integer Programs with Octagonal Loops
+Normal rank
@@ Property / cites work @@
+Q4418693
@@ Property / cites work: Q4418693 / rank @@
+Normal rank
@@ Property / cites work @@
+Taming Past LTL and Flat Counter Systems
@@ Property / cites work: Taming Past LTL and Flat Counter Systems / rank @@
+Normal rank
@@ Property / cites work @@
+On the Complexity of Verifying Regular Properties on Flat Counter Systems,
+Normal rank
@@ Property / cites work @@
+Equivalence Between Model-Checking Flat Counter Systems and Presburger Arithmetic
+Normal rank
@@ Property / cites work @@
+Model-checking CTL* over flat Presburger counter systems
+Normal rank
@@ Property / cites work @@
+“Sometimes” and “not never” revisited
@@ Property / cites work: “Sometimes” and “not never” revisited / rank @@
+Normal rank
@@ Property / cites work @@
+Modalities for model checking: Branching time logic strikes back
+Normal rank
@@ Property / cites work @@
+Q4415251
@@ Property / cites work: Q4415251 / rank @@
+Normal rank
@@ Property / cites work @@
+Proving safety properties of infinite state systems by compilation into Presburger arithmetic
+Normal rank
@@ Property / cites work @@
+Branching-Time Model Checking of Parametric One-Counter Automata
+Normal rank
@@ Property / cites work @@
+Branching-Time Model Checking of One-Counter Processes and Timed Automata
+Normal rank
@@ Property / cites work @@
+Subclasses of presburger arithmetic and the weak EXP hierarchy
+Normal rank
@@ Property / cites work @@
+Reachability in Succinct and Parametric One-Counter Automata
+Normal rank
@@ Property / cites work @@
+The strong exponential hierarchy collapses
@@ Property / cites work: The strong exponential hierarchy collapses / rank @@
+Normal rank
@@ Property / cites work @@
+Reversal-Bounded Multicounter Machines and Their Decision Problems
+Normal rank
@@ Property / cites work @@
+Q2771058
@@ Property / cites work: Q2771058 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4608681
@@ Property / cites work: Q4608681 / rank @@
+Normal rank
@@ Property / cites work @@
+TaPAS: The Talence Presburger Arithmetic Suite
@@ Property / cites work: TaPAS: The Talence Presburger Arithmetic Suite / rank @@
+Normal rank
@@ Property / cites work @@
+CONCUR 2004 - Concurrency Theory
@@ Property / cites work: CONCUR 2004 - Concurrency Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Technology for Verification and Analysis
+Normal rank
@@ Property / cites work @@
+Persistence of vector replacement systems is decidable
+Normal rank
@@ Property / cites work @@
+Q5590814
@@ Property / cites work: Q5590814 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4298260
@@ Property / cites work: Q4298260 / rank @@
+Normal rank
@@ Property / cites work @@
+Verification Decidability of Presburger Array Programs
+Normal rank