Paper Info
Title
Fully-Abstract Statecharts Semantics via Intuitionistic Kripke Models
Abstract
The semantics of Statecharts macro steps, as introduced by Pnueli and Shalev, lacks compositionality. This paper first analyzes the compositionality problem and traces it back to the invalidity of the Law of the Excluded Middle. It then characterizes the semantics via a particular class of linear, intuitionistic Kripke models, namely stabilization sequences. This yields, for the first time in the literature, a simple fully-abstract semantics which interprets Pnueli and Shalev's concept of failure naturally. The results not only give insights into the semantic subtleties of Statecharts, but also provide a basis for developing algebraic theories for macro steps and for comparing different Statecharts variants.
Year
DOI
Venue
2000
10.1007/3-540-45022-X_14
ICALP
Keywords
Field
DocType
stabilization sequence,particular class,intuitionistic kripke models,statecharts macro step,semantic subtlety,simple fully-abstract semantics,intuitionistic kripke model,algebraic theory,macro step,compositionality problem,fully-abstract statecharts semantics,different statecharts variant
Principle of compositionality,Kripke structure,Specification language,Intuitionistic logic,Programming language,Algebraic number,Law of excluded middle,Computer science,Macro,Semantics
Conference
Volume
ISSN
ISBN
1853
0302-9743
3-540-67715-1
Citations 
PageRank 
References 
4
0.55
11
Authors
2
Name
Order
Citations
PageRank
Gerald Lüttgen160040.71
Michael Mendler231434.60