Name
Title | ||
|---|---|---|
Compositional nonblocking verification for extended finite-state automata using partial unfolding |
Abstract | ||
|---|---|---|
This paper describes a framework for compositional nonblocking verification of discrete event systems modelled as extended finite-state automata. Compositional verification is shown in previous work to be efficient to verify the nonblocking property of large discrete event systems. Here, these results are applied to extended finite-state automata communicating via shared variables and events. The model to be verified is composed gradually, partially unfolding variables as needed. At each step, symbolic observation equivalence is used to simplify the resultant components in such a way that the final verification result is the same as it would have been for the original model. The paper concludes with an example showing the potential of compositional verification to achieve substantial state-space reduction. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1109/CoASE.2013.6654014 | Automation Science and Engineering |
Keywords | Field | DocType |
discrete event systems,finite state machines,state-space methods,compositional nonblocking verification,discrete event systems,extended finite-state automata,partial unfolding,shared events,shared variables,state-space reduction,symbolic observation equivalence | Shared variables,Discrete event dynamic system,Automaton,Theoretical computer science,Finite-state machine,Equivalence (measure theory),Mathematics | Conference |
ISSN | Citations | PageRank |
2161-8070 | 3 | 0.46 |
References | Authors | |
8 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sahar Mohajerani | 1 | 37 | 5.18 |
| Robi Malik | 2 | 253 | 26.13 |
| Martin Fabian | 3 | 204 | 27.91 |