Extended Transition Systems for Parametric Bisimulation

n this work we have defined a parametric model for describing the semantics of finite states systems. It relies on the parametric theories of observation trees [5, 6] and proved trees [8]. A notion of parametric bisimulation is introduced over extended transition systems and it is shown that this equivalence coincide with the ones already presented in literature. The results presented in this paper are fundamental for a practical use of a parametric theory in automatic verification of systems. Following the definitions given above, it is immediate to derive an algorithm for parametric bisimulation when incremental observations are considered. The extension to other observations is under development following the approach of decomposing any non-incremental observation into an incremental one and an abstraction function. The basic idea is use standard techniques from fix-point theory to prove properties on regular languages that may permit to make this decomposition effective.