On Algorithms For LLTS Ready Simulation

Process algebras and temporal logics are two most widely used specification systems in concurrency theory. The former supports compositional specification while the latter is good at descripting and verifying abstract properties of the system. Recently, Gerald Luttgen et al. combined both to propose the notion of logic labeled transition system and corresponding refinement relation —— LLTS ready simulation. Such notion provides a unified framework for operational and logical specifications by introducing conjunction into normal labeled transition system and correspondingly tagging inconsistent processes arising from conjunct with a predicate, and hence has powerful expressiveness. Moreover, the LLTS ready simulation is the largest precongruence w.r.t. parallel composition and conjunction. This paper aims to provide an algorithm for LLTS ready simulations. Our main work includes:1. Introduce the notion of stability of the partition pair, and then prove the equivalence between stable partition pair and LLTS ready simulation. Depend on such equivalence, we translate the problem for deciding LLTS ready simulation into solving the so called “coarsest partition” problem, and give a operator r which could be used to solve our problem; we also prove the correctness of this procedure.2. From a more generalized standpoint, we propose the concept of generalized ready simulation which is equivalent to LLTS ready simulation. Based on this concept we present the definition of generalized stability of partition pair and corresponding coarsest generalized stable refinement, and then reveal that there exists certain isomorphism between generalized ready simulation and generalized stable partition pair.3. We give a more efficient way to determine the generalized stability of a partition pair based on the notions of “partition stability” and “relation stability”. Finally, we present the algorithm ERS and consider its correctness and complexity.