Research On The LLTS-oriented Process Calculus CLL_R

The dominant approaches for the specification, verification and systematic development of reactive and concurrent systems are based on either states or actions. Action-based approaches put attention to behavior of systems, which have tended to use formalisms in algebraic style. There formalisms are referred to as process algebra or process calculus. State-based approaches devote themselves to specifying and verifying abstract properties of systems, which often involve logic languages (e.g., modal logic,μ-calculus). These two approaches take different standpoint for looking at specifications and verifications, and offer complementary advantages. In order to take advantage of these two approaches when designing systems, so-called heterogeneous specifications have been proposed. Among them, the notion of the logic labelled transition system (LLTS for short) has been introduced and explored by Luttgen and Vogler, which overcomes drawbacks existing in other heterogeneous specifications, and admits the free mixing of usual operational operators, logic operators and temporal operators.Hitherto LLTS has been explored in considerable depth, however, a few fundamental problems are still open. This thesis intends to study these problems in a pure process-algebraic style. Our contributions include:(1) We provide a process calculus CLLR for LLTS. This calculus not only rephrases Luttgen and Vogler’s semantic constructions (except hiding operator) in a pure process-algebraic style but also develops the general theory concerning (nested) recursive operations over LLTS. The latter is not considered by Luttgen and Vogler. Based on exploring the relationship between context, unfolding of recursion and transition relation in detail, we develop the behavioural theory of CLLR and prove that the ready simulation relation is precongruence w.r.t all operators in CLLR, which reveals that CLLR supports compositional reasoning. As an LLTS-oriented calculus, CLLR has to deal with inconsistency caused by conjunction of processes. Since the consistency of processes is sensitive to divergence, it is more difficult to deal with recursion in CLLR than one in usual process calculus.(2) We provide an axiomatic system AXCLL for CLLR, and prove that this system is sound and ground-complete for the processes without recursion. In effect, AXCLL gives an axiomatization of Luttgen and Vogler’s ready simulation in the presence of logic operators.(3) We study equations of the form X= tx in CLLR and establish Unique Solution Theorem and Greatest Solution Theorem. The former gives a sufficient condition for equations so that they have a unique solution, and the latter reveals the relationship between the recursive process<X‖X= tx> and solutions of equation X=RS tx, more precisely, it asserts that <X‖X= tx> is the loosest one among solutions of X=RS tx whenever X is strongly guarded in tx.(4) As an application of recursive operator, we provide a method to encode a fragment of action-based CTL (ACTL for short) into CLLR. This encoding simplifies Luttgen and Vogler’s temporal constructions greatly. Such result also supports to claim that the safety properties of the universal fragment of ACTL could be expressed within CLL^ in a natural manner, and the model checking of these properties may be reduced to implementation verification between CLLR-processes.In a word, this work not only lifts Luttgen and Vogler’work to a process-algebraic setting but also explores issues, such as, recursive operator and its behaviour theory, solutions of equations and axiomatization, that are not considered by them. Compared with usual process calculi, it is one distinguishing feature of CLLR that it involves consideration of conjunction of processes and inconsistencies caused by conjunction; moreover, CLLR supports compositional reasoning and allows ones to use operational operators, recursion, logical operators and modal operators freely when designing systems.