The complexity of live sequence charts

Yves Bontemps, Pierre Yves Schobbens

Research output: Contribution in Book/Catalog/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publication8th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2005
Pages364-378
Number of pages15
Volume3441
Publication statusPublished - 19 Sep 2005
Event8th 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 - Edinburgh, United Kingdom
Duration: 4 Apr 20058 Apr 2005

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
ISSN (Print)0302-9743

Conference

Conference8th 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
CountryUnited Kingdom
CityEdinburgh
Period4/04/058/04/05

Fingerprint Dive into the research topics of 'The complexity of live sequence charts'. Together they form a unique fingerprint.

Cite this