Paper Info
Title
Symbolic Reachability Analysis of FIFO Channel Systems with Nonregular Sets of Configurations (Extended Abstract)
Abstract
We address the verification problem of FIFO-channel systems by applying the symbolic analysis principle. We represent their sets of states (configurations) using structures called CQDD's combining finitestate automata with linear constraints on number of occurrences of symbols. We show that CQDD's allow forward and backward reachability analysis of systems with nonregular sets of configurations. Moreover, we prove that CQDD's allow to compute the exact effect of the repeated execution of any fixed cycle in the transition graph of a system. We use this fact to define a generic reachability analysis semi-algorithm parametrized by a set of cycles . Given a set of configurations, this semi-algorithm performs a least fixpoint calculation to construct the set of its successors (or predecessors). At each step, this calculation is accelerated by considering the cycles in as additional meta-transitions in the transition graph, generalizing the approach adopted in [5].
Year
DOI
Venue
1997
10.1007/3-540-63165-8_211
ICALP
Keywords
Field
DocType
fifo channel systems,extended abstract,symbolic reachability analysis,nonregular sets,symbolic analysis
FIFO (computing and electronics),Computer science,Communication channel,Theoretical computer science,Reachability
Conference
ISBN
Citations 
PageRank 
3-540-63165-8
25
1.30
References 
Authors
16
2
Name
Order
Citations
PageRank
Ahmed Bouajjani12663184.84
Peter Habermehl250230.39