Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-05089-3_9
Title: Fair model checking with process counter abstraction
Authors: Sun, J. 
Liu, Y. 
Roychoudhury, A. 
Liu, S. 
Dong, J.S. 
Issue Date: 2009
Source: Sun, J.,Liu, Y.,Roychoudhury, A.,Liu, S.,Dong, J.S. (2009). Fair model checking with process counter abstraction. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 5850 LNCS : 123-139. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-05089-3_9
Abstract: Parameterized systems are characterized by the presence of a large (or even unbounded) number of behaviorally similar processes, and they often appear in distributed/concurrent systems. A common state space abstraction for checking parameterized systems involves not keeping track of process identifiers by grouping behaviorally similar processes. Such an abstraction, while useful, conflicts with the notion of fairness. Because process identifiers are lost in the abstraction, it is difficult to ensure fairness (in terms of progress in executions) among the processes. In this work, we study the problem of fair model checking with process counter abstraction. Even without maintaining the process identifiers, our on-the-fly checking algorithm enforces fairness by keeping track of the local states from where actions are enabled / executed within an execution trace. We enhance our home-grown PAT model checker with the technique and show its usability via the automated verification of several real-life protocols. © 2009 Springer-Verlag Berlin Heidelberg.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/40025
ISBN: 3642050883
ISSN: 03029743
DOI: 10.1007/978-3-642-05089-3_9
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

20
checked on Dec 5, 2017

Page view(s)

49
checked on Dec 9, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.