کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
426504 | 686088 | 2010 | 23 صفحه PDF | دانلود رایگان |
![عکس صفحه اول مقاله: Ready simulation for concurrency: It’s logical! Ready simulation for concurrency: It’s logical!](/preview/png/426504.png)
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 [TCS 373 (1–2) 19–40] to the standard setting of labelled transition systems with (CSP-style) 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.
Journal: Information and Computation - Volume 208, Issue 7, July 2010, Pages 845-867