Affordable Access

Publisher Website

Liveness Checking as Safety Checking for Infinite State Spaces

Authors
Journal
Electronic Notes in Theoretical Computer Science
1571-0661
Publisher
Elsevier
Publication Date
Volume
149
Issue
1
Identifiers
DOI: 10.1016/j.entcs.2005.11.018
Keywords
  • Liveness
  • Safety
  • Linear Temporal Logic
  • Model Checking
  • Infinite State Space
Disciplines
  • Mathematics

Abstract

Abstract In previous work we have developed a syntactic reduction of repeated reachability to reachability for finite state systems. This may lead to simpler and more uniform proofs for model checking of liveness properties, help to find shortest counterexamples, and overcome limitations of closed-source model-checking tools. In this paper we show that a similar reduction can be applied to a number of infinite state systems, namely, ( ω−)regular model checking, push-down systems, and timed automata.

There are no comments yet on this publication. Be the first to share your thoughts.