2016
Composing constraint automata, state-by-state
Publication
Publication
The grand composition of n automata may have a number of states/transitions exponential in n. When it does, it seems not unreasonable for the computation of that grand composition to require exponentially many resources (time, space, or both). Conversely, if the grand composition of n automata has a number of states/transitions only linear in n, we may reasonably expect the computation of that grand composition to also require only linearly many resources. Recently and problematically, we saw cases of linearly-sized grand compositions whose computation required exponentially many resources. We encountered these cases in the context of Reo (a graphical language for coordinating components in component-based software), constraint automata (a general formalism for modeling systems’ behavior), and our compiler for Reo based on constraint automata. Combined with earlier research on constraint automata verification, these ingredients facilitate a correctness-by-construction approach to component-based software engineering—one of the hallmarks in Sifakis’ “rigorous system design”. To achieve that ambitious goal, however, we need to solve the previously stated problem. In this paper we present such a solution.
| Additional Metadata | |
|---|---|
| doi.org/10.1007/978-3-319-28934-2_12 | |
| International Workshop on Formal Aspects of Component Software | |
| Detection and Diagnosis of Deviations in Distributed Systems of Autonomous Agents | |
| Organisation | Computer Security |
|
Jongmans, S., Kappé, T., & Arbab, F. (2016). Composing constraint automata, state-by-state. Presented at the International Workshop on Formal Aspects of Component Software. doi:10.1007/978-3-319-28934-2_12 |
|
