publication . Article . Conference object . Other literature type . 2002

Liveness Checking as Safety Checking

Armin Biere;
Open Access
  • Published: 01 Dec 2002 Journal: Electronic Notes in Theoretical Computer Science, volume 66, issue 2, pages 160-177 (issn: 1571-0661, Copyright policy)
  • Publisher: Elsevier BV
  • Country: Sweden
Abstract
AbstractTemporal logic is widely used for specifying hardware and software systems. Typically two types of properties are distinguished, safety and liveness properties. While safety can easily be checked by reachability analysis, and many efficient checkers for safety properties exist, more sophisticated algorithms have always been considered to be necessary for checking liveness. In this paper we describe an efficient translation of liveness checking problems into safety checking problems. A counter example is detected by saving a previously visited state in an additional state recording component and checking a loop closing condition. The approach handles fair...
Subjects
ACM Computing Classification System: TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
free text keywords: Computer Sciences, Datavetenskap (datalogi), Theoretical Computer Science, Computer Science(all), General Computer Science
Related Organizations
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue