Options
A linear-time branching-time perspective on interface automata
Vogler, Walter; Lüttgen, Gerald (2020): A linear-time branching-time perspective on interface automata, in: Acta Informatica, Springer, Jg. 57, Nr. 3, S. 513–550, doi: 10.1007/s00236-020-00369-4.
Faculty/Chair:
Author:
Title of the Journal:
Acta Informatica
ISSN:
1432-0525
0001-5903
Publisher Information:
Year of publication:
2020
Volume:
57
Issue:
3
Pages:
Language:
English
Abstract:
Over the past two decades, de Alfaro and Henzinger’s interface automata (IA) have become a popular formal framework for the component-based specification of concurrent systems. IA’s parallel composition assumes that a component may wait on inputs but never on outputs, implying that an output must be consumed immediately or a communication error occurs. By now, the literature contains a number of semantics for IA: linear-time semantics based on traces observing communication errors, quiescence and/or divergence, as well as branching-time semantics based on alternating simulation. This article surveys these semantics from Rob van Glabbeek’s linear-time branching-time perspective, which does not consider settings with communication errors. We shed light onto the subtleties implied by IA’s pruning of all behaviour that might lead a component to autonomously enter an error state, and investigate when exactly de Alfaro and Henzinger’s restriction of input-determinism is needed. In addition, we introduce several new semantics for IA, in particular the linear-time ready semantics and the branching-time ready simulation.
GND Keywords: ; ; ; ;
Mensch-Maschine-Schnittstelle
Semantik
Computersimulation
Constraint <Künstliche Intelligenz>
Framework <Informatik>
Keywords: ; ; ; ;
interface automata
semantics
simulation
de Alfaro and Henzinger’s restriction
Glabbeek’s linear-time branching-time perspective
DDC Classification:
RVK Classification:
Peer Reviewed:
Yes:
International Distribution:
Yes:
Type:
Article
Activation date:
July 6, 2021
Versioning
Question on publication
Permalink
https://fis.uni-bamberg.de/handle/uniba/50150