{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T21:41:00Z","timestamp":1760218860504,"version":"build-2065373602"},"reference-count":54,"publisher":"MDPI AG","issue":"3","license":[{"start":{"date-parts":[[2014,7,8]],"date-time":"2014-07-08T00:00:00Z","timestamp":1404777600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Algorithms"],"abstract":"<jats:p>Temporal logic has become a well-established method for specifying the behavior of distributed systems. In this paper, we interpret a temporal logic over a partial order model that is a trace system. The satisfaction of the formulae is directly defined on traces on the basis of rewriting rules; so, the graph representation of the system can be completely avoided; moreover, a method is presented that keeps the trace system finite, also in the presence of infinite computations. To further reduce the complexity of model checking temporal logic formulae, an abstraction technique is applied to trace systems.<\/jats:p>","DOI":"10.3390\/a7030339","type":"journal-article","created":{"date-parts":[[2014,7,8]],"date-time":"2014-07-08T11:15:26Z","timestamp":1404818126000},"page":"339-362","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Model Checking Properties on Reduced Trace Systems"],"prefix":"10.3390","volume":"7","author":[{"given":"Antonella","family":"Santone","sequence":"first","affiliation":[{"name":"Dipartimento di Ingegneria, Universit\u00e0 del Sannio, Benevento 82100, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gigliola","family":"Vaglini","sequence":"additional","affiliation":[{"name":"Dipartimento di Ingegneria della Informazione, Universit\u00e0 di Pisa, Pisa 56122, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2014,7,8]]},"reference":[{"key":"ref_1","unstructured":"Manna, Z., and Pnueli, A. (June, January 30). The anchored version of the temporal framework. Proceedings of the Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School\/Workshop, Noordwijkerhout, The Netherlands. Lecture Notes in Computer Science."},{"key":"ref_2","unstructured":"Emerson, E.A., and Srinivasan, J. (June, January 30). Branching time temporal logic. Proceedings of the Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School\/Workshop, Noordwijkerhout, The Netherlands. Lecture Notes in Computer Science."},{"key":"ref_3","unstructured":"Mazurkiewicz, A. (June, January 30). Basic notions of Trace Theory. Proceedings of the Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School\/Workshop, Noordwijkerhout, The Netherlands. Lecture Notes in Computer Science."},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/0304-3975(89)90052-2","article-title":"Concurrent systems and inevitability","volume":"281","author":"Mazurkiewicz","year":"1989","journal-title":"Theor. Comput. Sci."},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic verification of finite-state concurrent systems using temporal logic verification","volume":"8","author":"Clarke","year":"1986","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for boolean function manipulation","volume":"C-35","author":"Bryant","year":"1986","journal-title":"IEEE Trans. Comput."},{"key":"ref_7","unstructured":"Burch, J., Clarke, E., McMillan, K., Dill, D., and Hwang, L. (1990, January 4\u20137). Symbolic Model Checking: 1020 States and Beyond. Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, Philadelphia, PA, USA."},{"key":"ref_8","first-page":"343","article-title":"Model checking and abstraction","volume":"16","author":"Clarke","year":"1992","journal-title":"Trans. Program. Lang. Syst."},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","article-title":"CADP 2011: A toolbox for the construction and analysis of distributed processes","volume":"15","author":"Garavel","year":"2013","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"ref_10","doi-asserted-by":"crossref","unstructured":"Godefroid, P. (1996). Partial-Order Methods for the Verification of Concurrent Systems, Springer. Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-60761-7"},{"key":"ref_11","doi-asserted-by":"crossref","unstructured":"Barbuti, R., de Francesco, N., Santone, A., and Vaglini, G. (1997, January 18\u201321). Selective mu-calculus: New modal operators for proving properties on reduced transition systems. Proceedings of the FORTE X\/PSTV XVII \u201997, Osaka, Japan.","DOI":"10.1007\/978-0-387-35271-8_32"},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"537","DOI":"10.1006\/jcss.1999.1660","article-title":"Selective mu-calculus and formula-based equivalence of transition systems","volume":"59","author":"Barbuti","year":"1999","journal-title":"J. Comput. Syst. Sci."},{"key":"ref_13","unstructured":"Stirling, C. (1989, January 25\u201327). An Introduction to Modal and Temporal Logics for CCS. Proceedings of the UK\/Japan Workshop on Concurrency : Theory, Language, and Architecture, Oxford, UK. Lecture Notes in Computer Science."},{"key":"ref_14","doi-asserted-by":"crossref","unstructured":"De Nicola, R., and Vaandrager, F.W. (1990, January 23\u201327). Action versus State based Logics for Transition Systems. Proceedings of the LITP Spring School on Theoretical Computer Science on Semantics of Systems of Concurrent Processes, La Roche Posay, France. Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-53479-2_17"},{"key":"ref_15","first-page":"279","article-title":"Trace Theory","volume":"Volume 255","author":"Mazurkiewicz","year":"1987","journal-title":"Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course"},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1016\/0304-3975(92)90183-G","article-title":"Local model checking for infinite state spaces","volume":"157","author":"Bradfield","year":"1992","journal-title":"Theor. Comput. Sci."},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., and Pnueli, A. (1985, January 14\u201316). Checking that finite state concurrent programs satisfy their linear specification. Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL \u201985), New Orleans, LA, USA.","DOI":"10.1145\/318593.318622"},{"key":"ref_18","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","article-title":"The complexity of propositional linear time logics","volume":"32","author":"Sistla","year":"1985","journal-title":"J. ACM"},{"key":"ref_19","unstructured":"Godefroid, P., and Piterman, N. (2009, January 18\u201320). LTL Generalized Model Checking Revisited. Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI \u201909), Savannah, GA, USA. Lecture Notes in Computer Science."},{"key":"ref_20","doi-asserted-by":"crossref","unstructured":"Diekert, V., and Rozenberg, G. (1995). The Book of Traces, Chapter Infinite Traces, World Scientific.","DOI":"10.1142\/9789814261456"},{"key":"ref_21","first-page":"31","article-title":"Temporal logics for trace systems: On automated verification","volume":"4","author":"Penczek","year":"1993","journal-title":"Int. J. Comput. Sci."},{"key":"ref_22","doi-asserted-by":"crossref","unstructured":"Bradfield, J. (1996, January 26\u201329). The modal mu-calculus alternation hierarchy is strict. Proceedings of the 7th International Conference CONCUR\u201996, Pisa, Italy.","DOI":"10.1007\/3-540-61604-7_58"},{"key":"ref_23","doi-asserted-by":"crossref","unstructured":"Chieu, D.V., and Hung, D.V. (2010, January 7\u20139). An extension of Mazukiewicz traces and their applications in specification of real-time systems. Proceedings of the Second International Conference on Knowledge and Systems Engineering (KSE \u201910), Hanoi, The Netherlands.","DOI":"10.1109\/KSE.2010.39"},{"key":"ref_24","unstructured":"Kupferman, O., and Vardi, M.Y. (1998, January 8\u201312). Relating Linear and Branching Model Checking. Proceedings of the IFIP TC2\/WG2.2, 2.3 International Conference on Programming Concepts and Methods (PROCOMET \u201998), Shelter Island, NY, USA."},{"key":"ref_25","unstructured":"Kupferman, O., and Vardi, M.Y. (1998, January 21\u201324). Freedom, weakness, and determinism: From linear-time to branching-time. Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS \u201998), Indianapolis, IN, USA."},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"McMillan, K.L. (1995, January 3\u20135). Trace theoretic verification of asynchronous circuits using unfoldings. Proceedings of the 7th International Conference on Computer-Aided Verification (CAV \u201995), Liege, Belgium. Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-60045-0_50"},{"key":"ref_27","unstructured":"Wallner, F. (July, January 28). Model checking LTL using net unfoldings. Proceedings of the 10th International Conference on Computer-Aided Verification (CAV \u201998), Vancouver, BC, Canada. Lecture Notes in Computer Science."},{"key":"ref_28","unstructured":"McMillan, K.L. (July, January 29). Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. Proceedings of the 4th International Workshop on Computer-Aided Verification (CAV \u201992), Montreal, QC, Canada. Lecture Notes in Computer Science."},{"key":"ref_29","unstructured":"Bollig, B., and Leucker, M. (2001, January 14\u201316). Deciding LTL over Mazurkiewicz Traces. Proceedings of the Symposium on Temporal Representation and Reasoning (TIME \u201901), Cividale, Italy."},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"Kaivola, R. (1995, January 11\u201313). A simple decision method for the linear time mu-calculus. Proceedings of the International Workshop on Structures in Concurrency Theory (STRICT), Berlin, Germany. Workshops in Computing.","DOI":"10.1007\/978-1-4471-3078-9_13"},{"key":"ref_31","unstructured":"Thiagarajan, P.S., and Walukiewicz, I. (July, January 29). An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces. Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS \u201997), Warsaw, Poland."},{"key":"ref_32","doi-asserted-by":"crossref","unstructured":"Walukiewicz, I. (2000). Local Logics of Traces, BRICS. BRICS Report RS-00-2.","DOI":"10.7146\/brics.v7i2.20130"},{"key":"ref_33","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Pnueli, A., and Raviv, L. (1998, January 13\u201317). Algorithmic Verification of Linear Temporal Logic Specifications. Proceedings of the 25th International Colloquium on Automata, Languages and Programming (ICALP \u201998), Aalborg, Denmark. Lecture Notes in Computer Science.","DOI":"10.1007\/BFb0055036"},{"key":"ref_34","unstructured":"Peled, D. (July, January 28). All from one, one from all: On model checking using representatives. Proceedings of the 5th International Conference on Computer-Aided Verification, (CAV \u201993), Elounda, Greece. Lecture Notes in Computer Science."},{"key":"ref_35","doi-asserted-by":"crossref","unstructured":"Dumas, X., Boniol, F., Dhaussy, P., and Bonnafous, E. (2010, January 7\u20139). Context Modelling and Partial-Order Reduction: Application to SDL Industrial Embedded Systems. Proceedings of the IEEE Fifth International Symposium on Industrial Embedded Systems (SIES \u201910), Trento, Italy.","DOI":"10.1109\/SIES.2010.5551396"},{"key":"ref_36","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1016\/j.cosrev.2010.06.002","article-title":"Linear temporal logic symbolic model checking","volume":"5","author":"Rozier","year":"2011","journal-title":"Comput. Sci. Rev."},{"key":"ref_37","doi-asserted-by":"crossref","first-page":"1130","DOI":"10.1016\/j.ic.2006.10.009","article-title":"When not losing is better than winning: Abstraction and refinement for the full mu-calculus","volume":"205","author":"Grumberg","year":"2007","journal-title":"Inf. Comput."},{"key":"ref_38","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1007\/s10009-011-0202-1","article-title":"Local abstraction-refinement for the \u03bc-calculus","volume":"13","author":"Fecher","year":"2011","journal-title":"Softw. Tools Technol. Transf."},{"key":"ref_39","doi-asserted-by":"crossref","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., and Schwoon, S. (2000, January 15\u201319). Efficient Algorithms for Model Checking Pushdown Systems. Proceedings of the 12th International Conference on Computer-Aided Verification (CAV \u201900), Chicago, IL, USA. Lecture Notes in Computer Science.","DOI":"10.1007\/10722167_20"},{"key":"ref_40","first-page":"62","article-title":"Pushdown processes: Games and Model Checking","volume":"Volume 1102","author":"Walukiewicz","year":"1996","journal-title":"Proceedings of the 8th International Conference on Computer Aided Verification (CAV \u201996)"},{"key":"ref_41","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1016\/j.tcs.2007.03.049","article-title":"Complexity results on branching-time pushdown model checking","volume":"379","author":"Bozzelli","year":"2007","journal-title":"Theor. Comput. Sci."},{"key":"ref_42","unstructured":"Carotenuto, D., Murano, A., and Peron, A. (2007, January 3\u20136). 2-Visibly Pushdown Automata. Proceedings of the 11th International Conference on Developments in Language Theory (DLT \u201907), Turku, Finland."},{"key":"ref_43","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Piterman, N., and Vardi, M.Y. (2002, January 14\u201318). Pushdown Specifications. Proceedings of the 9th International Conference, LPAR, Tbilisi, Georgia.","DOI":"10.1007\/3-540-36078-6_18"},{"key":"ref_44","doi-asserted-by":"crossref","unstructured":"L\u00f6ding, C., and Rohde, P. (2003, January 15\u201317). Model Checking and Satisfiability for Sabotage Modal Logic. Proceedings of the 23rd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS \u201903), Mumbai, India.","DOI":"10.1007\/978-3-540-24597-1_26"},{"key":"ref_45","unstructured":"Hutter, D., and Werner, S. (2002). Festschrift in Honour of J\u00f6rg Siekmann, LNAI, Springer."},{"key":"ref_46","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1006\/inco.2000.2893","article-title":"Module checking","volume":"164","author":"Kupferman","year":"2001","journal-title":"Inf. Comput."},{"key":"ref_47","first-page":"36","article-title":"Module checking revisited","volume":"Volume 1254","author":"Kupferman","year":"1997","journal-title":"Proceedings of the 9th International Conference (CAV\u00e2\u0080\u009997)"},{"key":"ref_48","first-page":"1","article-title":"Algorithms for omega-regular games with imperfect information","volume":"3","author":"Chatterjee","year":"2007","journal-title":"Log. Methods Comput. Sci."},{"key":"ref_49","first-page":"504","article-title":"Pushdown module checking","volume":"Volume 3835","author":"Bozzelli","year":"2005","journal-title":"Proceedings of the 12th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR \u201905)"},{"key":"ref_50","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/s10703-010-0093-x","article-title":"Pushdown module checking, Form","volume":"36","author":"Bozzelli","year":"2010","journal-title":"Methods Syst. Des."},{"key":"ref_51","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.ic.2012.11.005","article-title":"Pushdown module checking with imperfect information","volume":"223","author":"Aminof","year":"2013","journal-title":"Inf. Comput."},{"key":"ref_52","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1016\/j.ic.2011.10.008","article-title":"Improved model checking of hierarchical systems","volume":"210","author":"Aminof","year":"2012","journal-title":"Inf. Comput."},{"key":"ref_53","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1145\/503502.503503","article-title":"Model checking of hierarchical state machines","volume":"23","author":"Alur","year":"2001","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"ref_54","doi-asserted-by":"crossref","first-page":"786","DOI":"10.1145\/1075382.1075387","article-title":"Analysis of recursive state machines","volume":"27","author":"Alur","year":"2005","journal-title":"ACM Trans. Program. Lang. Syst."}],"container-title":["Algorithms"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1999-4893\/7\/3\/339\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T21:13:22Z","timestamp":1760217202000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1999-4893\/7\/3\/339"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7,8]]},"references-count":54,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2014,9]]}},"alternative-id":["a7030339"],"URL":"https:\/\/doi.org\/10.3390\/a7030339","relation":{},"ISSN":["1999-4893"],"issn-type":[{"type":"electronic","value":"1999-4893"}],"subject":[],"published":{"date-parts":[[2014,7,8]]}}}