TY - GEN
T1 - The complexity of live sequence charts
AU - Bontemps, Yves
AU - Schobbens, Pierre Yves
PY - 2005/9/19
Y1 - 2005/9/19
N2 - We are interested in implementing a fully automated software development process starting from sequence charts, which have proven their naturalness and usefulness in industry. We show in this paper that even for the simplest variants of sequence charts, there are strong impediments to the implementability of this dream. In the case of a manual development, we have to check the final implementation (the model). We show that centralized model-checking is co-NP-complete. Unfortunately, this problem is of little interest to industry. The real problem is distributed model-checking, that we show PSPACE complete, as well as several simple but interesting verification problems. The dream itself relies on program synthesis, formally called realizability. We show that the industrially relevant problem, distributed realizability, is undecidable. The less interesting problems of centralized and constrained realizability are exponential and doubly-exponential complete, respectively.
AB - We are interested in implementing a fully automated software development process starting from sequence charts, which have proven their naturalness and usefulness in industry. We show in this paper that even for the simplest variants of sequence charts, there are strong impediments to the implementability of this dream. In the case of a manual development, we have to check the final implementation (the model). We show that centralized model-checking is co-NP-complete. Unfortunately, this problem is of little interest to industry. The real problem is distributed model-checking, that we show PSPACE complete, as well as several simple but interesting verification problems. The dream itself relies on program synthesis, formally called realizability. We show that the industrially relevant problem, distributed realizability, is undecidable. The less interesting problems of centralized and constrained realizability are exponential and doubly-exponential complete, respectively.
UR - http://www.scopus.com/inward/record.url?scp=24644449798&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:24644449798
VL - 3441
T3 - Lecture Notes in Computer Science
SP - 364
EP - 378
BT - 8th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2005
T2 - 8th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005
Y2 - 4 April 2005 through 8 April 2005
ER -