Subtyping is a crucial ingredient of session type theory and its applications, notably to programming language implementations. In this paper, we study effective ways to check whether a session type is a subtype of another by applying a characteristic formulae approach to the problem. Our core contribution is an algorithm to generate a modal mu-calculus formula that characterises all the supertypes (or subtypes) of a given type. Subtyping checks can then be off-loaded to model checkers, thus incidentally yielding an efficient algorithm to check safety of session types, soundly and completely. We have implemented our theory and compared its cost with other classical subtyping algorithms.
Characteristic formulae for finite processes were first studied in @cite_23 , then in @cite_12 for finite-state processes. Since then the theory has been studied extensively @cite_19 @cite_36 @cite_37 @cite_11 @cite_27 @cite_10 @cite_9 for most of the van Glabbeek's spectrum @cite_15 and in different settings (e.g., time @cite_31 and probabilistic @cite_13 ). See @cite_9 @cite_37 for a detailed historical account of the field. This is the first time characteristic formulae are applied to the field of session types. A recent work @cite_9 proposes a general framework to obtain characteristic formula constructions for simulation-like relation for free''. We chose to follow @cite_12 as it was a better fit for session types as they allow for a straightforward inductive construction of a characteristic formula. Moreover, @cite_12 uses the standard @math -calculus which allowed us to integrate our theory with an existing model checker.
@cite_13 @cite_37 @cite_31 @cite_36 @cite_9 @cite_19 @cite_27 @cite_23 @cite_15 @cite_10 @cite_12 @cite_11
180602404 2111205369 2025280888 1968829301 2133147428 1550474961
Recently, a general framework on characteristic formulae was proposed by It offers a simple theory that allows one to easily obtain characteristic formulae of many non-probabilistic behavioral relations. Our paper studies their techniques in a probabilistic setting. We provide a general method for determining characteristic formulae of behavioral relations for probabilistic automata using fixed-point probability logics. We consider such behavioral relations as simulations and bisimulations, probabilistic bisimulations, probabilistic weak simulations, and probabilistic forward simulations. This paper shows how their constructions and proofs can follow from a single common technique. This paper offers characteristic formula constructions in the real-time logic L ν for several behavioural relations between (states of) timed automata. The behavioural relations studied in this work are timed (bi)similarity, timed ready simulation, faster-than bisimilarity and timed trace inclusion. The characteristic formulae delivered by our constructions have size which is linear in that of the timed automaton they logically describe. This also applies to the characteristic formula for timed bisimulation equivalence, for which an exponential space construction was previously offered by Laroussinie, Larsen and Weise. Abstract Characteristic formulae have been introduced by Graf and Sifakis to relate equational reasoning about proceses to reasoning in a modal logic, and therefore to allow proofs about processes to be carried out in a logical framework. This work, which concerned finite processes and bisimulation-like equivalences, has later on been extended to finite state processes and further equivalences. Based upon an intuitionistic understanding of Hennessy-Milner Logic (HML) with mutual recursion, we extend these results to cover bisimulation-like preorders, which are sensitive to liveness properties. This demonstrates the expressive power of intuitionistically interpreted HML with mutual recursion, and it builds the theoretical basis for a uniform and efficient method to automatically verify bisimulation-like relations between processes by means of model checking. We propose a translation method of finite terms of CCS into formulas of a modal language representing their class of observational congruence. For this purpose, we define a modal language and a function associating with any finite term of CCS a formula of the language, satisfied by the term. Furthermore, this function is such that two terms are congruent if and only if the corresponding formulas are equivalent. The translation method consists in associating with operations on terms (action, +) operations on the corresponding formulas. This work is a first step towards the definition of a modal language with modalities expressing both possibility and inevitability and which is compatible with observational congruence. Abstract This paper shows how modal mu-calculus formulae characterizing finite-state processes up to strong or weak bisimulation can be derived directly from the well-known greatest fixpoint characterizations of the bisimulation relations. Our derivation simplifies earlier proofs for the strong bisimulation case and, by virtue of derivation, immediately generalizes to various other bisimulation-like relations, in particular weak bisimulation. This paper develops a model-checking algorithm for a fragment of the modal mu-calculus and shows how it may be applied to the efficient computation of behavioral relations between processes. The algorithm's complexity is proportional to the product of the size of the process and the size of the formula, and thus improves on the best existing algorithm for such a fixed point logic. The method for computing preorders that the model checker induces is also more efficient than known algorithms.