Error-pruning in interface automata

De Alfaro and Henzinger introduced interface automata to model and study behavioural types. These come with alternating simulation as refinement and with a specific parallel composition: if one component receives an unexpected input, this is regarded as an error and the resp. error states are removed with a special pruning operation. In this paper, we return to the foundations of interface automata and study how refinement and parallel composition should be defined best. We take as basic requirement that an implementation must be error-free, if the specification is. For three variants of error-free, we consider the coarsest precongruence for parallel composition respecting the basic requirement. We find that pruning proves to be relevant in all cases and point out an important subtlety for systems that are not input-deterministic.

Authors

• Ferenc Bujtor
• Walter Vogler

Keywords

• Concurrency
• Interface automata
• Parallel composition
• Optimistic/pessimistic approach
• Fully abstract precongruence