ON REACHABILITY AND SAFETY IN INFINITE-STATE SYSTEMS

DOI10.1142/S0129054101000898zbMath1319.68084OpenAlexW2067723582MaRDI QIDQ5249293

Jianwen Su, Tevfik Bultan, Oscar H. Ibarra

Publication date: 30 April 2015

Published in: International Journal of Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1142/s0129054101000898

zbMATH Keywords

invariantsreachabilityinfinite-state systemsautomated verification

Mathematics Subject Classification ID

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

Related Items (4)

On store languages and applications ⋮ When Is Reachability Intrinsically Decidable? ⋮ INDUCTIVE COMPOSITION OF NUMBERS WITH MAXIMUM, MINIMUM, AND ADDITION: A New Theory for Program Execution-Time Analysis ⋮ Semilinearity of Families of Languages

Cites Work

• Model-checking in dense real-time
• Recursive unsolvability of Post's problem of Tag und other topics in theory of Turing machines
• The complexity of decision problems for finite-turn multicounter machines
• Symbolic model checking: \(10^{20}\) states and beyond
• A theory of timed automata
• Symbolic model checking for real-time systems
• A technique for proving decidability of containment and equivalence of linear constraint queries
• Decidability of model checking for infinite-state concurrent systems
• Reversal-Bounded Multicounter Machines and Their Decision Problems
• A really temporal logic
• A variant of a recursively unsolvable problem

This page was built for publication: ON REACHABILITY AND SAFETY IN INFINITE-STATE SYSTEMS