The operational semantics of interactive systems is usually described bylabeled transition systems. Abstract semantics (that is defined in terms ofbisimilarity) is characterized by the final morphism in some category ofcoalgebras. Since the behaviour of interactive systems is for many reasonsinfinite, symbolic semantics were introduced as a mean to define smaller,possibly finite, transition systems, by employing symbolic actions and avoidingsome sources of infiniteness. Unfortunately, symbolic bisimilarity has adifferent shape with respect to ordinary bisimilarity, and thus the standardcoalgebraic characterization does not work. In this paper, we introduce itscoalgebraic models. We will use as motivating examples two asynchronousformalisms: open Petri nets and asynchronous pi-calculus. Indeed, as we haveshown in a previous paper, asynchronous bisimilarity can be seen as an instanceof symbolic bisimilarity.
展开▼
