×

Ready simulation for concurrency: it’s logical! (English) Zbl 1197.68053

Summary: This article provides new insight into the connection between the trace-based lower part of van Glabbeek’s linear-time, branching-time spectrum and its simulation-based upper part. We establish that ready simulation is fully abstract with respect to failure inclusion, when adding the conjunction operator that was proposed by the authors in [Theor. Comput. Sci. 373, No. 1–2, 19–40 (2007; Zbl 1111.68085)] to the standard setting of labelled transition systems with parallel composition. More precisely, we actually prove a stronger result by considering a coarser relation than failure inclusion, namely a preorder that relates processes with respect to inconsistencies that may arise under conjunctive composition.
Ready simulation is also shown to satisfy standard logic properties. In addition, our semantic formalism proves itself robust when adding disjunction, external choice and hiding operators, and is thus suited for studying mixed operational and logic languages. Finally, the utility of our formalism is demonstrated by means of a small example that deals with specifying and reasoning about mode logics within aircraft control systems.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B70 Logic in computer science
93C95 Application models in control theory

Citations:

Zbl 1111.68085

Software:

LOTOS
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Bergstra, J.; Ponse, A.; Smolka, S., Handbook of Process Algebra (2001), Elsevier · Zbl 0971.00006
[2] Hoare, C., Communicating Sequential Processes (1985), Prentice Hall · Zbl 0637.68007
[3] Milner, R., Communication and Concurrency (1989), Prentice Hall · Zbl 0683.68008
[4] Emerson, E., Temporal and modal logic, (Handbook of Theoretical Computer Science, vol. B (1990), North-Holland), 995-1072 · Zbl 0900.03030
[5] Lüttgen, G.; Vogler, W., Conjunction on processes: full-abstraction via ready-tree semantics, (FOSSACS 2006. FOSSACS 2006, LNCS, vol. 3921 (2006), Springer), 261-276 · Zbl 1180.68196
[6] Lüttgen, G.; Vogler, W., Conjunction on processes: full-abstraction via ready-tree semantics, TCS, 373, 1-2, 19-40 (2007) · Zbl 1111.68085
[7] Glabbeek, R., The linear time — branching time spectrum I, (Handbook of Process Algebra (2001), Elsevier), 3-99, (Chapter 1) · Zbl 1035.68073
[8] Veglioni, S.; De Nicola, R., Possible worlds for process algebras, (CONCUR ’98. CONCUR ’98, LNCS, vol. 1466 (1998), Springer), 179-193
[9] Brookes, S.; Hoare, C.; Roscoe, A., A theory of communicating sequential processes, J. ACM, 31, 3, 560-599 (1984) · Zbl 0628.68025
[10] Bolognesi, T.; Brinksma, E., Introduction to the ISO specification language LOTOS, Comput. Networks, 14, 25-59 (1987)
[11] Bloom, B.; Istrail, S.; Meyer, A., Bisimulation can’t be traced, J. ACM, 42, 1, 232-268 (1995) · Zbl 0886.68027
[12] Olderog, E.-R., Nets, terms and formulas, (Cambridge Tracts in Theoretical Computer Science, vol. 23 (1991), Cambridge University Press) · Zbl 0741.68002
[13] Steen, M.; Derrick, J.; Boiten, E.; Bowman, H., Consistency of partial process specifications, (AMAST ’98. AMAST ’98, LNCS, vol. 1548 (1999), Springer), 248-262
[14] Olderog, E.-R.; Hoare, C., Specification-oriented semantics for communicating processes, Acta Inform., 23, 1, 9-66 (1986) · Zbl 0569.68019
[16] Ulidowski, I., Equivalences on observable processes, (LICS ’92 (1992), IEEE Computer Society Press), 148-159
[17] Ulidowski, I., Refusal simulation and interactive games, (AMAST 2002. AMAST 2002, LNCS, vol. 2422 (2002), Springer), 208-222 · Zbl 1275.68107
[19] Graf, S.; Sifakis, J., A logic for the description of non-deterministic programs and their properties, Inform. Control, 68, 1-3, 254-270 (1986) · Zbl 0591.68017
[20] Lamport, L., The temporal logic of actions, TOPLAS, 16, 3, 872-923 (1994)
[21] Abadi, M.; Plotkin, G., A logical view of composition, TCS, 114, 1, 3-30 (1993) · Zbl 0778.68061
[22] Kurshan, R., Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach (1994), Princeton University Press
[23] Raclet, J.-B., Residual for component specifications, (Formal Aspects of Component Software. Formal Aspects of Component Software, ENTCS, vol. 215 (2008), Elsevier), 93-110
[24] Dill, D., Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits (1988), MIT Press
[25] de Alfaro, L.; Henzinger, T., Interface automata, (FSE 2001 (2001), ACM Press), 109-120
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.