Paper Info
Title
Verifying Universal Properties of Parameterized Networks
Abstract
We present a method for verifying universal properties of fair parameterized networks of finite processes, that is, properties of the form ∀p1... pn: ψ, where ψ is a quantifier-free LTL formula. The starting point of our verification method is an encoding of the infinite family of networks by a single fair transition system whose variables are set (2nd- order) variables and transitions are described in WS1S, such a system is called a WS1S transition system. We abstract the WS1S system into a finite state system that can be model-checked. We present a generic abstraction relation for verifying universal properties as well as an algorithm for computing an abstract system. Since, the abstract system may contain infinite computations that have no corresponding fair computations at the concrete level, the verification of progress property often fails. Therefore, we present methods that allow to synthesize fairness conditions from the parameterized network and discuss under which conditions and how to lift fairness conditions of this network to fairness conditions on the abstract system. We implemented our methods in a tool, called pax, and applied it to several examples.
Year
DOI
Venue
2000
10.1007/3-540-45352-0_24
FTRTFT
Keywords
Field
DocType
corresponding fair computation,ws1s system,verifying universal properties,ws1s transition system,fairness condition,universal property,abstract system,present method,single fair transition system,fair parameterized network,finite state system,parameterized networks
Transition system,Parameterized complexity,Algorithm,Theoretical computer science,Finite-state machine,Smoothing,Linear logic,Temporal logic,Mathematics,Computation,Encoding (memory)
Conference
Volume
ISSN
ISBN
1926
0302-9743
3-540-41055-4
Citations 
PageRank 
References 
10
0.64
15
Authors
3
Name
Order
Citations
PageRank
Kai Baukus11015.21
Yassine Lakhnech291378.50
Karsten Stahl3924.67