A divide and conquer approach to model checking of liveness properties

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

4 Scopus citations

Abstract

An approach to making liveness model checking problems under fairness feasible is described. The proposed method divides such a problem into multiple smaller ones that can be conquered such that the former is derived from the latter. Since the proposed method does not need any specialized algorithms, it can use existing LTL model checkers such as Spin, SAL and Maude LTL model checker. The proposed method also lets (or helps) humans get better understanding of the reason why they need to use fairness assumptions.

Original languageEnglish
Title of host publicationProceedings - 2013 IEEE 37th Annual Computer Software and Applications Conference, COMPSAC 2013
PublisherIEEE Computer Society
Pages648-657
Number of pages10
ISBN (Print)9780769549866
DOIs
StatePublished - 2013
Externally publishedYes
Event2013 IEEE 37th Annual Computer Software and Applications Conference, COMPSAC 2013 - Kyoto, Japan
Duration: 22 Jul 201326 Jul 2013

Publication series

NameProceedings - International Computer Software and Applications Conference
ISSN (Print)0730-3157

Conference

Conference2013 IEEE 37th Annual Computer Software and Applications Conference, COMPSAC 2013
Country/TerritoryJapan
CityKyoto
Period22/07/1326/07/13

Keywords

  • Fairness
  • Liveness property
  • Model checking
  • State machine

Fingerprint

Dive into the research topics of 'A divide and conquer approach to model checking of liveness properties'. Together they form a unique fingerprint.

Cite this