Name
Title | ||
|---|---|---|
A Kleene theorem and model checking algorithms for existentially bounded communicating automata |
Abstract | ||
|---|---|---|
The behavior of a network of communicating automata is called existentially bounded if communication events can be scheduled in such a way that the number of messages in transit is always bounded by a value that depends only on the machine, not the run itself. We show a Kleene theorem for existentially bounded communicating automata, namely the equivalence between communicating automata, globally cooperative compositional message sequence graphs, and monadic second order logic. Our characterization extends results for universally bounded models, where for each and every possible scheduling of communication events, the number of messages in transit is uniformly bounded. As a consequence, we give solutions in spirit of Madhusudan (2001) for various model checking problems on networks of communicating automata that satisfy our optimistic restriction. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1016/j.ic.2006.01.005 | Inf. Comput. |
Keywords | Field | DocType |
bounded model,various model checking problem,model checking,communicating finite state machines,model checking algorithm,possible scheduling,cooperative compositional message sequence,kleene theorem,order logic,68n30,optimistic restriction,communication event,message sequence charts,satisfiability,message sequence chart | Discrete mathematics,Combinatorics,Model checking,Scheduling (computing),Uniform boundedness,Algorithm,Finite-state machine,Equivalence (measure theory),Message sequence chart,Monadic predicate calculus,Mathematics,Bounded function | Journal |
Volume | Issue | ISSN |
204 | 6 | Information and Computation |
Citations | PageRank | References |
40 | 1.38 | 25 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Blaise Genest | 1 | 304 | 25.09 |
| Dietrich Kuske | 2 | 485 | 47.93 |
| Anca Muscholl | 3 | 1179 | 74.92 |