The classical model for concurrent systems is based on observing execution sequences of global states, separated from each other by atomic transitions. This model is intuitively simple and enjoys a variety of mathematical tools, e.g., finite automata and linear temporal logic, and algorithms that can be applied in order to test and verify concurrent systems. Although this model is sufficient for most frequently used validation tasks, some phenomena of concurrent systems are difficult to express using its related formalisms. In particular, not all the global states (snapshots) related to an execution appear on a particular execution sequence; some appear on equivalent sequences. Previous attempts to move into formalisms that are based on a more detailed model of execution, e.g,. the causality based model, resulted in specification formalisms with inherently high complexity verification algorithms. We study here verification problems that involve allowing the execution sequences model to observe past global states from equivalent executions. We show various algorithms and complexity results related to our extension of the interleaving model.
- 5.Alur, R., Peled, D., Penczek, W.: Model-Checking of Causality Properties. In: LICS 1995, pp. 90–100 (1995)Google Scholar
- 10.Emerson, E.A., Jutla, C.S.: The complexity of Tree Automata and Logics of Programs. In: FOCS 1988 (1988)Google Scholar
- 14.Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly Automatic Verification of Linear Temporal Logic. In: PSTV 1995, pp. 3–18 (1995)Google Scholar
- 16.Peled, D., Pnueli, A.: Proving Partial Order Liveness Properties. In: ICALP 1990, pp. 553–571 (1990)Google Scholar
- 18.Mazurkiewicz, A.: Trace semantics. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 255, pp. 279–324. Springer, Heidelberg (1987)Google Scholar
- 20.Peled, D.: Specification and Verification of Message Sequence Charts. In: FORTE/PSTV 2000, pp. 139–154 (2000)Google Scholar
- 22.Plandowski, W., Rytter, W.: Complexity of Language Recognition Problems for Compressed Words. In: Jewels are Forever, pp. 262–272. Springer, Heidelberg (1999)Google Scholar