Ferenc Bujtor, Universität Augsburg
De Alfaro and Henzinger developed interface automata to model and study behavioural types, which describe communication patterns of systems while abstracting from data. They stipulate a parallel composition with a built-in removal of errors due to unexpected inputs, and alternating bisimulation as refinement relation.
We considered the usual parallel composition and retain errors. Our basic criterion for refinement was “if the specification is error free, the implementation should be as well”. Our first notion of error freeness – an error must not be reached by internal and output actions alone – fits to the optimistic understanding of errors in interface automata. We characterized the coarsest precongruence, which proved correct the parallel composition of De Alfaro and Henzinger, but also showed that their refinement is unnecessarily strict.
In this talk we expand on our fundamental studies by considering two other notions of error freeness: the hyper-optimistic internal approach, where an error is problematic only if it is reached by internal actions alone, and a pessimistic approach also found in literature, where any reachable error is problematic. For each we describe a precongruence, which turns out to be considerably more complicated than the optimistic one.
Surprisingly both these precongruences are strictly finer than the optimistic one and their underlying semantics use a similar treatment of errors.