A compositional semantics for statecharts using labeled transition systems

Andrew C. Uselton; Scott A. Smolka

doi:10.1007/978-3-540-48654-1_2

A compositional semantics for statecharts using labeled transition systems

Andrew C. Uselton
, Scott A. Smolka

Computer Science

Stony Brook University

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

38 Scopus citations

Abstract

We characterize the statecharts step semantics of Pnueli and Shalev as a mapping Ψ from an inductively defined algebra of statecharts terms to a domain of labeled transition systems (LTSs). Statecharts equivalence =_sc, i.e. LTS isomorphism, is shown not to be a congruence and hence the step semantics is not compositional. We define a new semantic mapping Ψ_> to a domain of LTSs with a richer label structure, and show that LTS isomorphism in this domain is the largest congruence contained in =_sc.

Original language	English
Title of host publication	CONCUR 1994
Subtitle of host publication	Concurrency Theory - 5th International Conference, Proceedings
Editors	Bengt Jonsson, Joachim Parrow
Publisher	Springer Verlag
Pages	2-17
Number of pages	16
ISBN (Print)	9783540583295
DOIs	https://doi.org/10.1007/978-3-540-48654-1_2
State	Published - 1994
Event	5th International Conference on Concurrency Theory, CONCUR 1994 - Uppsala, Sweden Duration: Aug 22 1994 → Aug 25 1994

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	836 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	5th International Conference on Concurrency Theory, CONCUR 1994
Country/Territory	Sweden
City	Uppsala
Period	08/22/94 → 08/25/94

Access to Document

10.1007/978-3-540-48654-1_2

Cite this

Uselton, A. C., & Smolka, S. A. (1994). A compositional semantics for statecharts using labeled transition systems. In B. Jonsson, & J. Parrow (Eds.), CONCUR 1994: Concurrency Theory - 5th International Conference, Proceedings (pp. 2-17). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 836 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-540-48654-1_2

Uselton, Andrew C. ; Smolka, Scott A. / A compositional semantics for statecharts using labeled transition systems. CONCUR 1994: Concurrency Theory - 5th International Conference, Proceedings. editor / Bengt Jonsson ; Joachim Parrow. Springer Verlag, 1994. pp. 2-17 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{15104084cf5c41038e54a715fe0c94dd,

title = "A compositional semantics for statecharts using labeled transition systems",

abstract = "We characterize the statecharts step semantics of Pnueli and Shalev as a mapping Ψ from an inductively defined algebra of statecharts terms to a domain of labeled transition systems (LTSs). Statecharts equivalence =sc, i.e. LTS isomorphism, is shown not to be a congruence and hence the step semantics is not compositional. We define a new semantic mapping Ψ> to a domain of LTSs with a richer label structure, and show that LTS isomorphism in this domain is the largest congruence contained in =sc.",

author = "Uselton, \{Andrew C.\} and Smolka, \{Scott A.\}",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1994.; 5th International Conference on Concurrency Theory, CONCUR 1994 ; Conference date: 22-08-1994 Through 25-08-1994",

year = "1994",

doi = "10.1007/978-3-540-48654-1\_2",

language = "English",

isbn = "9783540583295",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "2--17",

editor = "Bengt Jonsson and Joachim Parrow",

booktitle = "CONCUR 1994",

}

Uselton, AC & Smolka, SA 1994, A compositional semantics for statecharts using labeled transition systems. in B Jonsson & J Parrow (eds), CONCUR 1994: Concurrency Theory - 5th International Conference, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 836 LNCS, Springer Verlag, pp. 2-17, 5th International Conference on Concurrency Theory, CONCUR 1994, Uppsala, Sweden, 08/22/94. https://doi.org/10.1007/978-3-540-48654-1_2

A compositional semantics for statecharts using labeled transition systems. / Uselton, Andrew C.; Smolka, Scott A.
CONCUR 1994: Concurrency Theory - 5th International Conference, Proceedings. ed. / Bengt Jonsson; Joachim Parrow. Springer Verlag, 1994. p. 2-17 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 836 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - A compositional semantics for statecharts using labeled transition systems

AU - Uselton, Andrew C.

AU - Smolka, Scott A.

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 1994.

PY - 1994

Y1 - 1994

N2 - We characterize the statecharts step semantics of Pnueli and Shalev as a mapping Ψ from an inductively defined algebra of statecharts terms to a domain of labeled transition systems (LTSs). Statecharts equivalence =sc, i.e. LTS isomorphism, is shown not to be a congruence and hence the step semantics is not compositional. We define a new semantic mapping Ψ> to a domain of LTSs with a richer label structure, and show that LTS isomorphism in this domain is the largest congruence contained in =sc.

AB - We characterize the statecharts step semantics of Pnueli and Shalev as a mapping Ψ from an inductively defined algebra of statecharts terms to a domain of labeled transition systems (LTSs). Statecharts equivalence =sc, i.e. LTS isomorphism, is shown not to be a congruence and hence the step semantics is not compositional. We define a new semantic mapping Ψ> to a domain of LTSs with a richer label structure, and show that LTS isomorphism in this domain is the largest congruence contained in =sc.

UR - https://www.scopus.com/pages/publications/0039101842

U2 - 10.1007/978-3-540-48654-1_2

DO - 10.1007/978-3-540-48654-1_2

M3 - Conference contribution

AN - SCOPUS:0039101842

SN - 9783540583295

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 2

EP - 17

BT - CONCUR 1994

A2 - Jonsson, Bengt

A2 - Parrow, Joachim

PB - Springer Verlag

T2 - 5th International Conference on Concurrency Theory, CONCUR 1994

Y2 - 22 August 1994 through 25 August 1994

ER -

Uselton AC, Smolka SA. A compositional semantics for statecharts using labeled transition systems. In Jonsson B, Parrow J, editors, CONCUR 1994: Concurrency Theory - 5th International Conference, Proceedings. Springer Verlag. 1994. p. 2-17. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-48654-1_2

A compositional semantics for statecharts using labeled transition systems

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this