Paper Info
Title
Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems
Abstract
Compositional generation is an incremental technique for generating a reduced labelled transition system representing the behaviour of a set of communicating processes. In particular, since intermediate reductions can be performed after each generation step, the size of the Lts can be kept small and state-explosion can be av oided in many cases. This paper deals with compositional generation in presence of asynchronous communications via shared buffers. More precisely, we show how partial-order reduction techniques can be used in this context to define equivalence relations: that preserve useful properties, are congruence w.r.t asynchronous composition, and rely on a (syntactic) notion of preorder on execution sequences characterizing their "executability" in any buffer environment. Two such equivalences are proposed, together with dedicated asynchronous composition operators able to directly produce reduced Lts.
Year
Venue
Keywords
2000
TACAS
compositional state space generation,congruence w,dedicated asynchronous composition operator,incremental technique,equivalence relation,generation step,partial order reductions,reduced labelled transition system,asynchronous communicating systems,asynchronous composition,buffer environment,compositional generation,asynchronous communication,partial order reduction,state space
Field
DocType
Volume
Transition system,Asynchronous communication,Equivalence relation,Computer science,Preorder,Formal specification,Theoretical computer science,Operator (computer programming),Congruence (geometry),Formal verification,Distributed computing
Conference
1785
ISSN
ISBN
Citations 
0302-9743
3-540-67282-6
7
PageRank 
References 
Authors
0.54
15
2
Name
Order
Citations
PageRank
Jean-pierre Krimm116310.57
Laurent Mounier2118779.54