Research On Label-Structured Transition Systems Based On Institution

As a classic formal model, labelled transition systems(LTS, for short) have been used to describe the behavior of concurrent systems widely. But the structure of labels does not been considered in the classic transition systems. When one study on concurrent system with special requirements, a more complex transition system is needed, as its formal model. For some specific areas or issues, academics have proposed a number of transition systems with quantitative informations on their labels or actions. In this paper, we enrich LTS with partial order over labels, called label-structured transition systems(LSTS, for short), which is a common form of the sort of transition systems with quantitative informations.In the context of institution theory, this thesis research on several issues in the framework of label-structured transition systems. Main results include:(1) Based on the notion of the label-structured transition systems, we present notions of label-structured partial bisimulations and label-structured covariant–contravariant simulations, and establish the logical characteristics of them using the modal logic languages BL and C CL.(2) We show that LSTS can be turned into institutions in modal logic languages BL and C CL, with label-structured partial bisimulations and label-structured covariant–contravariant simulations as there morphisms(denoted by p bI and c cI), respectively. Similarly, label-structured modal transition systems can be turned into an institution in modal logic languages M T SL, with label-structured modal refinement as there morphisms(denoted by m t sI).(3) We explore the relationship among p bI, c cI and m t sI. In particular, we show that there exist institution morphisms from p bI and m t sI to c cI respectively. The result indicates that label-structured covariant-contravariant simulation over LSTS is more expressive than the others.