publication . Part of book or chapter of book . Article . 1999

Extended abstract

Ahmed Bouajjani; Peter Habermehl;
Open Access
  • Published: 01 Jun 1999
  • Publisher: Springer Berlin Heidelberg
Abstract We address the verification problem of FIFO-channel systems. We apply the symbolic analysis principle to these systems. We represent their sets of configurations using structures called constrained queue-content decision diagrams (CQDDs) combining finite-state automata with linear arithmetical constraints on number of occurrences of symbols. We show that CQDDs allow forward and backward reachability analysis of systems with nonregular sets of configurations. Moreover, we prove that CQDDs 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 an...
free text keywords: Verification, Infinite-state systems, FIFO-channel systems, Symbolic reachability analysis, Non-regular sets, Automata, Linear constraints, Theoretical Computer Science, Computer Science(all), General Computer Science
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue