Taming past LTL and flat counter systems

DOI10.1016/j.ic.2015.03.007zbMath1378.68112OpenAlexW2034462340MaRDI QIDQ2346416

Arnaud Sangnier, Amit Kumar Dhar, Stéphane P. Demri

Publication date: 1 June 2015

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2015.03.007

zbMATH Keywords

complexitymodel-checkingflatnesssmall solutionPresburger arithmeticsystem of equationslinear-time temporal logicstutteringcounter system

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Temporal logic (03B44)

Related Items (5)

Forward analysis and model checking for trace bounded WSTS ⋮ Verification of Flat FIFO Systems ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Model-Checking Counting Temporal Logics on Flat Structures

Uses Software

• FLATA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Stutter-invariant temporal properties are expressible without the next-time operator
• The covering and boundedness problems for vector addition systems
• Specification in CTL + past for verification in CTL.
• An until hierarchy and other applications of an Ehrenfeucht-Fraïssé game for temporal logic
• The stuttering principle revisited
• Model-checking CTL* over flat Presburger counter systems
• Taming Past LTL and Flat Counter Systems
• Safety Problems Are NP-complete for Flat Integer Programs with Octagonal Loops
• Weak Kripke Structures and LTL
• Reachability in Succinct and Parametric One-Counter Automata
• Equivalence Between Model-Checking Flat Counter Systems and Presburger Arithmetic
• Integer Vector Addition Systems with States
• Temporal Logic with Capacity Constraints
• Towards SMT Model Checking of Array-Based Systems
• Fast Acceleration of Ultimately Periodic Relations
• Towards Model-Checking Programs with Lists
• The complexity of propositional linear temporal logics
• Bounds on Positive Integral Solutions of Linear Diophantine Equations
• Log Space Recognition and Translation of Parenthesis Languages
• Alternating automata: Unifying truth and validity checking for temporal logics
• On the Complexity of Verifying Regular Properties on Flat Counter Systems,
• Automated Technology for Verification and Analysis
• Flat Parametric Counter Automata

This page was built for publication: Taming past LTL and flat counter systems