| [1] |
Ben-Ari M (2006) Principles of concurrent and distributed programming, 2nd edn. Addison-Wesley, Harlow · Zbl 0701.68001 |
| [2] |
Bäumler S, Balser M, Nafz F, Reif W, Schellhorn G (2010) Interactive verification of concurrent systems using symbolic execution.. AI Commun 23(2-3): 285-307 · Zbl 1205.68217 |
| [3] |
Baier C, Katoen J-P (2008) Principles of model checking. MIT Press, Cambridge, MA · Zbl 1179.68076 |
| [4] |
Bäumler S, Schellhorn G, Tofan B, Reif W (2011) Proving linearizability with temporal logic.. Form Asp Comput 23(1): 91-112 · Zbl 1214.68209 · doi:10.1007/s00165-009-0130-y |
| [5] |
Cerny E, Dudani S, Havlicek J, Korchemny D (2015) SVA: the power of assertions in systemVerilog, 2nd edn. Springer, Cham |
| [6] |
Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge, MA · Zbl 1423.68002 |
| [7] |
Chellas BF (1980) Modal logic: an introduction. Cambridge University Press, Cambridge, UK · Zbl 0431.03009 |
| [8] |
Van Hung D (January 2000) Projections: A technique for verifying real-time programs in DC. Technical report 178, UNU/IIST, Macau, 1999. Also in proceedings of conference on information technology and education, Ho Chi Minh city, Vietnam · Zbl 1256.03023 |
| [9] |
Volker D, Gastin P (2008) First-order definable languages. In: Flum J, Grädel E, Wilke T (eds) Logic and automata: history and perspectives, volume 2 of texts in logic and games. Amsterdam University Press, Amsterdam, pp 261-306 · Zbl 1234.03024 |
| [10] |
Duan Z, Koutny M, Holt C (1994) Projection in temporal logic programming. In: Pfennig F (ed) LPAR ’94, volume 822 of LNCS. Springer, Berlin, pp 333-344 |
| [11] |
Dax C, Klaedtke F, Leue S (2009) Specification languages for stutter-invariant regular properties. In: Liu Z, Ravn AP (eds) 7th International symposium on automated technology for verification and analysis (ATVA 2009), volume 5799 of LNCS. Springer, Berlin, pp 244-254 · Zbl 1262.68114 |
| [12] |
de Roever W-P, de Boer F, Hanneman U, Hooman J, Lakhnech Y, Poel M, Zwiers J (2001) Concurrency verification: introduction to compositional and noncompositional methods. Cambridge University Press, Cambridge · Zbl 1009.68020 |
| [13] |
Duan Z (1996) An extended interval temporal logic and a framing technique for temporal logic programming. PhD thesis, Department of Computing Science, Newcastle University, Newcastle upon Tyne, England, Tech. rep. 556 |
| [14] |
Duan Z, Yang X, Koutny M (2008) Framed temporal logic programming.. Sci Comput Progr 70(1): 31-61 · Zbl 1131.68036 · doi:10.1016/j.scico.2007.09.001 |
| [15] |
Eisner C, Fisman D (2006) A practical introduction to PSL. Springer, New York |
| [16] |
Eisner C, Fisman D (2015) Temporal logic made practical. http://www.cis.upenn.edu/ fisman/documents/EF_HBMC14.pdf, 2014. Accessed 4 June 2015. In: Clarke EM, Henzinger TA, Veith H (eds) Expected to appear in 2018 in Handbook of model checking. Springer, Cham · Zbl 1392.68247 |
| [17] |
Eisner C, Fisman D, Havlicek J, McIsaac A, Van Campenhout D (2003) The definition of a temporal clock operator. In: Baeten JCM, Lenstra JK, Parrow J, Woeginger GJ (eds) ICALP 2003, volume 2719 of LNCS. Springer, Berlin, pp 857-870 · Zbl 1039.03505 |
| [18] |
Allen EE (1990) Temporal and modal logic. In: van Leeuwen J (ed) Handbook of theoretical computer science, volume B: formal models and semantics, chapter 16. Elsevier/MIT Press, Amsterdam, pp 995-1072 · Zbl 1378.03017 |
| [19] |
Guelev DP, Van Hung D (2002) Prefix and projection onto state in duration calculus.. Electr Notes Theor Comput Sci 65(6): 101-119 · Zbl 1270.68169 · doi:10.1016/S1571-0661(04)80472-9 |
| [20] |
Guelev DP, Van Hung D (2004) A relatively complete axiomatisation of projection onto state in the duration calculus.. J Appl Non Class Log 14(1-2): 149-180 · Zbl 1181.03014 · doi:10.3166/jancl.14.149-180 |
| [21] |
Gelade W (2010) Succinctness of regular expressions with interleaving, intersection and counting.. Theor Comput Sci 411(31-33): 2987-2998 · Zbl 1192.68120 · doi:10.1016/j.tcs.2010.04.036 |
| [22] |
Gischer J (1981) Shuffle languages, Petri nets, and context-sensitive grammars.. Commun ACM 24(9): 597-605 · Zbl 0471.68063 · doi:10.1145/358746.358767 |
| [23] |
Gischer J (1988) The equational theory of pomsets.. Theor Comput Sci 61: 199-224 · Zbl 0669.68015 · doi:10.1016/0304-3975(88)90124-7 |
| [24] |
Godefroid P (1996) Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem, volume 1032 of LNCS. Springer, Berlin · Zbl 1293.68005 |
| [25] |
Guelev DP (2004) A complete proof system for first-order interval temporal logic with projection.. J Log Comput 14(2): 215-249 · Zbl 1070.03009 · doi:10.1093/logcom/14.2.215 |
| [26] |
Guelev DP (2004) Logical interpolation and projection onto state in the duration calculus.. J Appl Non Class Log 14(1-2): 181-208 · Zbl 1181.03013 · doi:10.3166/jancl.14.181-208 |
| [27] |
Godefroid P, Wolper P (1991) A partial approach to model checking. In: 6th Annual symposium on logic in computer science (LICS ’91). IEEE Computer Society, Los Alamitos, pp 406-415 · Zbl 0806.68079 |
| [28] |
Godefroid P, Wolper P (1991) Using partial orders for the efficient verification of deadlock freedom and safety properties. In: Larsen KG, Skou A (eds) 3rd International workshop on computer aided verification (CAV ’91), volume 575 of LNCS. Springer, Berlin, pp 332-342 · Zbl 0772.68064 |
| [29] |
Godefroid P, Wolper P (1993) Using partial orders for the efficient verification of deadlock freedom and safety properties.. Form Methods Syst Des 2(2): 149-164 · Zbl 0772.68064 · doi:10.1007/BF01383879 |
| [30] |
Hughes GE, Cresswell MJ (1996) A new introduction to modal logic. Routledge, London · Zbl 0855.03002 · doi:10.4324/9780203290644 |
| [31] |
He J (1999) A behavioral model for co-design. In: Wing JM, Woodcock J, Davies J (eds) FM’99, vol II, volume 1709 of LNCS. Springer, Berlin, pp 1420-1438 · Zbl 0948.03511 |
| [32] |
Halpern J, Manna Z, Moszkowski B (1983) A hardware semantics based on temporal intervals. In: Diaz J (ed) ICALP 1983, volume 154 of LNCS. Springer, Berlin, pp 278-291 · Zbl 0534.68025 |
| [33] |
Hollander Y, Morley M, Noy A (2001) The e language: a fresh separation of concerns. In: Proceedings of TOOLS Europe 2001: 38th internationa’l conference on technology of object-oriented languages and systems, components for mobile computing. IEEE Computer Society, Los Alamitos, pp 41-50 · Zbl 1181.03013 |
| [34] |
Holzmann G (2003) The SPIN model checker: primer and reference manual. Addison-Wesley Professional, Boston |
| [35] |
IEEE (2010) Standard for property specification language (PSL), standard 1850-2010. ANSI/IEEE, New York |
| [36] |
IEEE (2011) Standard for the functional verification language e, standard 1647-2011. ANSI/IEEE, New York |
| [37] |
IEEE (2012) Standard for systemVerilog—unified hardware design, specification, and verification language, standard 1800-2012. ANSI/IEEE, New York · Zbl 1270.68169 |
| [38] |
ISO (1986) Standard generalized markup language (SGML): ISO 8879:1986. International Organization for Standardization, Geneva, Switzerland · Zbl 1070.03009 |
| [39] |
ITL web pages. http://www.antonio-cau.co.uk/ITL/. Accessed 8 June 2015 · Zbl 0743.68097 |
| [40] |
Jones CB, Hayes IJ, Colvin RJ (2015) Balancing expressiveness in formal approaches to concurrency.. Form Asp Comput 27(3): 475-497 · Zbl 1343.68171 · doi:10.1007/s00165-014-0310-2 |
| [41] |
Jones CB (October 1983) Tentative steps toward a development method for interfering programs. ACM Trans Program Lang Syst 5(4):596-619 · Zbl 0517.68032 |
| [42] |
Keller RM (1976) Formal verification of parallel programs.. Commun ACM 19(7): 371-384 · Zbl 0329.68016 · doi:10.1145/360248.360251 |
| [43] |
Kröger F, Merz S (2008) Temporal logic and state systems. Texts in theoretical computer science (an EATCS series). Springer, Berlin · Zbl 0471.68063 |
| [44] |
Katz S, Peled D (1987) Interleaving set temporal logic. In: 6th Annual ACM symposium on principles of distributed computing (PODC ’87). ACM, New York, pp 178-190 · Zbl 0718.03014 |
| [45] |
Katz S, Peled DA (1990) Interleaving set temporal logic.. Theor Comput Sci 75(3): 263-287 · Zbl 0718.03014 · doi:10.1016/0304-3975(90)90096-Z |
| [46] |
Katz S, Peled DA (1992) Verification of distributed programs using representative interleaving sequences.. Distrib Comput 6(2): 107-120 · Zbl 0773.68053 · doi:10.1007/BF02252682 |
| [47] |
Lamport L (1983) What good is temporal logic? In: Mason REA (ed.) Information Processing 83, pp. 657-668. North-Holland, · Zbl 0669.68015 |
| [48] |
Lamport L (2002) Specifying Systems: The TLA+ language and tools for hardware and software engineers. Addison-Wesley Professional, Boston, MA, USA |
| [49] |
Lichtenstein O, Pnueli A, Zuck L (1985) The glory of the past. In: Parikh R (ed) Logics of Programs, volume 193 of LNCS. Springer, Berlin, pp 196-218 · Zbl 0586.68028 |
| [50] |
Moszkowski B, Guelev DP (2015) An application of temporal projection to interleaving concurrency. In: Li X, Liu Z, Yi W (eds) Dependable software engineering: theories, tools, and applications—first international symposium (SETTA 2015), volume 9409 in LNCS. Springer, Cham, pp 153-167 · Zbl 1369.68263 |
| [51] |
Moszkowski B, Manna Z (1984) Reasoning in interval temporal logic. In: Clarke EM, Kozen D (eds) Proceedings of workshop on logics of programs, Pittsburgh, PA, June, 1983, volume 164 of LNCS. Springer, Berlin, pp 371-382 · Zbl 0542.68022 |
| [52] |
Morley MJ (1999) Semantics of temporal e. In: Melham TF, Moller FG (eds) Banff’99 higher order workshop: formal methods in computation, Ullapool, Scotland, 9-11 Sept. 1999. Technical Report, Department of Computing Science, University of Glasgow, Glasgow, Scotland, pp 138-142 |
| [53] |
Moszkowski B (1983) Reasoning about digital circuits. PhD thesis, Department of Computer Science, Stanford University, June 1983. Technical report STAN-CS-83-970 |
| [54] |
Moszkowski B (1986) Executing temporal logic programs. Cambridge University Press, Cambridge · Zbl 0565.68003 |
| [55] |
Moszkowski B (1995) Compositional reasoning about projected and infinite time. In: Proceedings of 1st IEEE internationa’l conference on engineering of complex computer systems (ICECCS’95). IEEE Computer Society, Los Alamitos, pp 238-245 |
| [56] |
Moszkowski B (2000) An automata-theoretic completeness proof for interval temporal logic (extended abstract). In: Montanari U, Rolim J, Welzl E (eds) Proceedings of 27th international colloquium on automata, languages and programming (ICALP 2000), volume 1853 of LNCS. Springer, Berlin, pp 223-234 · Zbl 0973.03508 |
| [57] |
Moszkowski B (2004) A hierarchical completeness proof for propositional interval temporal logic with finite time. J Appl Non Class Log 14(1-2):55-104. Special issue on interval temporal logics and duration calculi. Goranko V, Montanari A, guest editors · Zbl 1181.03015 |
| [58] |
Moszkowski B (2012) A complete axiom system for propositional interval temporal logic, with infinite time.. Log Meth Comp Sci 8(3): 10-156 · Zbl 1256.03023 |
| [59] |
Moszkowski B (2013) Interconnections between classes of sequentially compositional temporal formulas.. Inf Process Lett 113(9): 350-353 · Zbl 1287.03074 · doi:10.1016/j.ipl.2013.02.005 |
| [60] |
Moszkowski B (2014) Compositional reasoning using intervals and time reversal.. Ann Math Artif Intell 71(1-3): 175-250 · Zbl 1378.03017 · doi:10.1007/s10472-013-9356-8 |
| [61] |
Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems: specifications. Springer, New York · Zbl 0753.68003 · doi:10.1007/978-1-4612-0931-7 |
| [62] |
Newcombe C, Rath T, Zhang F, Munteanu B, Brooker M, Deardeuff M (2015) How Amazon Web services uses formal methods.. Commun ACM 58(4): 66-73 · doi:10.1145/2699417 |
| [63] |
Olderog E-R, Dierks H (2008) Real-time systems: formal specification and automatic verification. Cambridge University Press, Cambridge · Zbl 1161.68030 · doi:10.1017/CBO9780511619953 |
| [64] |
Olderog E-R, Hoare CAR (1983) Specification-oriented semantics for communicating processes. In: Díaz J (ed) Automata, languages and programming, 10th colloquium (ICALP 1983), volume 154 of LNCS. Springer, Berlin, pp 561-572 · Zbl 0578.68009 |
| [65] |
Olderog E-R, Hoare CAR (1986) Specification-oriented semantics for communicating processes.. Acta Inf 23(1): 9-66 · Zbl 0569.68019 · doi:10.1007/BF00268075 |
| [66] |
OWL-S (2004) Semantic markup for web services. http://www.w3.org/Submission/OWL-S/. Accessed 14 March 2016 |
| [67] |
Peng F, Chen H (2015) Discovering restricted regular expressions with interleaving. In: Reynold C, Bin C, Zhenjie Z, Ruichu C, Jia X (eds) 17th Asia-Pacific Web conference on web technologies and applications (APWeb 2015), volume 9313 of LNCS. Springer, Cham, pp 104-115 |
| [68] |
Peng F, Chen H, Mou X (2015) Deterministic regular expressions with interleaving. In: Leucker M, Rueda C, Valencia FD (eds) 12th International colloquium on theoretical aspects of computing (ICTAC 2015), volume 9399 of LNCS. Springer, Cham, pp 203-220 · Zbl 1471.68120 |
| [69] |
Peled D (1993) All from one, one for all: on model checking using representatives. In: Costas Courcoubetis, (ed), 5th International conference on computer aided verification (CAV ’93), volume 697 of LNCS. Springer, Berlin, pp 409-423 |
| [70] |
Peled D (1996) Combining partial order reductions with on-the-fly model-checking.. Methods in System Design. 8(1): 39-64 · Zbl 1425.68267 · doi:10.1007/BF00121262 |
| [71] |
Peterson GL (1981) Myths about the mutual exclusion problem.. Inf Process Lett 12(3): 115-116 · Zbl 0474.68031 · doi:10.1016/0020-0190(81)90106-X |
| [72] |
Peled D, Wilke T (1997) Stutter-invariant temporal properties are expressible without the next-time operator.. Inf Process Lett 63(5): 243-246 · Zbl 1337.68170 · doi:10.1016/S0020-0190(97)00133-6 |
| [73] |
Schellhorn G, Tofan B, Ernst G, Pfähler J, Reif W (2014) RGITL: a temporal logic framework for compositional reasoning about interleaved programs. Ann Math Artif Intell 71(1-3):131-174 · Zbl 1329.68172 |
| [74] |
Taubenfeld G (2006) Synchronization algorithms and concurrent programming. Pearson/Prentice Hall, Harlow |
| [75] |
Valmari A (1991) Stubborn sets for reduced state space generation. In: Rozenberg G (ed) Advances in Petri nets 1990, volume 483 of LNCS. Springer, Berlin, pp 491-515 |
| [76] |
Valmari A (1992) A stubborn attack on state explosion.. Form Methods Syst Des 1(4): 297-322 · Zbl 0783.68083 · doi:10.1007/BF00709154 |
| [77] |
Yang C, Duan Z (2010) Compositional verification with stutter-invariant propositional projection temporal logic. In: Proceedings of the 14th WSEAS international conference on computers: part of the 14th WSEAS CSCC multiconference—volume I, ICCOMP’10. Stevens Point, Wisconsin, USA, World Scientific and Engineering Academy and Society (WSEAS), pp 272-280 |
| [78] |
Zhou C, Hansen MR (2004) Duration calculus: a formal approach to real-time systems. Springer, Berlin · Zbl 1071.68062 |
| [79] |
Zhou C, Hoare CAR, Ravn AP (1991) A calculus of durations.. Inf Process Lett 40(5): 269-276 · Zbl 0743.68097 · doi:10.1016/0020-0190(91)90122-X |
