{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T12:05:33Z","timestamp":1753877133279,"version":"3.41.2"},"reference-count":33,"publisher":"Oxford University Press (OUP)","license":[{"start":{"date-parts":[[2024,5,16]],"date-time":"2024-05-16T00:00:00Z","timestamp":1715817600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/pages\/standard-publication-reuse-rights"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>The distributed temporal logic (DTL) is a logic for reasoning about temporal properties of distributed systems from the local point of view of the system\u2019s agents, which are assumed to execute sequentially and to interact by means of synchronous event sharing. Different versions of DTL have been provided over the years for a number of different applications, reflecting different perspectives on how non-local information can be accessed by each agent. In this paper, we propose an automata-theoretic model checking algorithm for DTL. To this end, we propose a notion of distributed transition system that will be used to specify the system to be verified. The properties that the system should meet are specified in DTL. In order to capture the models of these properties, we propose the notions of generalized distributed B\u00fcchi automaton and of distributed B\u00fcchi automaton. With these concepts, we are able to adapt results from automata-theoretic approaches to model checking in LTL to the distributed case.<\/jats:p>","DOI":"10.1093\/jigpal\/jzae043","type":"journal-article","created":{"date-parts":[[2024,5,17]],"date-time":"2024-05-17T15:00:28Z","timestamp":1715958028000},"source":"Crossref","is-referenced-by-count":0,"title":["Model checking distributed temporal logic"],"prefix":"10.1093","author":[{"given":"Francisco","family":"Dion\u00edsio","sequence":"first","affiliation":[{"name":"Dep. Matem\u00e1tica, Instituto Superior T\u00e9cnico, Universidade de Lisboa , Portugal Instituto de Telecomunica\u00e7\u00f5es, Portugal, francisco.dionisio@tecnico.ulisboa.pt"}]},{"given":"Jaime","family":"Ramos","sequence":"additional","affiliation":[{"name":"Dep. Matem\u00e1tica, Instituto Superior T\u00e9cnico, Universidade de Lisboa , Portugal Instituto de Telecomunica\u00e7\u00f5es, Portugal, jaime.ramos@tecnico.ulisboa.pt"}]},{"given":"Fernando","family":"Subtil","sequence":"additional","affiliation":[{"name":"Dep. Matem\u00e1tica, Instituto Superior T\u00e9cnico, Universidade de Lisboa , Portugal, fmcsubtil@gmail.com"}]},{"given":"Luca","family":"Vigan\u00f2","sequence":"additional","affiliation":[{"name":"Department of Informatics , King\u2019s College London, London, UK, luca.vigano@kcl.ac.uk"}]}],"member":"286","published-online":{"date-parts":[[2024,5,16]]},"reference":[{"volume-title":"Principles of Model Checking","year":"2008","author":"Baier","key":"2024051714215170300_ref1"},{"key":"2024051714215170300_ref2","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1007\/s10009-016-0414-5","article-title":"Preface of the special issue on model checking of software","volume":"18","author":"Bartocci","year":"2016","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"2024051714215170300_ref3","first-page":"101","article-title":"A labeled tableaux for the distributed temporal logic DTL","volume-title":"Proceedings of the 15th Int. Symp. On Temporal Representation and Reasoning (TIME 2008)","author":"Basin","year":"2008"},{"key":"2024051714215170300_ref4","doi-asserted-by":"crossref","first-page":"1245","DOI":"10.1093\/logcom\/exp022","article-title":"Labelled tableaux for distributed temporal logic","volume":"19","author":"Basin","year":"2009","journal-title":"Journal of Logic and Computation"},{"key":"2024051714215170300_ref5","doi-asserted-by":"crossref","first-page":"4007","DOI":"10.1016\/j.tcs.2011.04.006","article-title":"Distributed temporal logic for the analysis of security protocol models","volume":"412","author":"Basin","year":"2011","journal-title":"Theoretical Computer Science"},{"key":"2024051714215170300_ref6","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-73483-0","volume-title":"Nonsequential Processes: A Petri Net View","author":"Best","year":"1988"},{"key":"2024051714215170300_ref7","doi-asserted-by":"crossref","first-page":"73","DOI":"10.4204\/EPTCS.124.8","article-title":"HyLTL: A temporal logic for model checking hybrid systems","volume":"124","author":"Bresolin","year":"2013","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"2024051714215170300_ref8","first-page":"73","article-title":"A tableaux-based decision procedure for distributed temporal logic","volume-title":"Essays in Honour of Amilcar Sernadas","author":"Caleiro","year":"2017"},{"key":"2024051714215170300_ref9","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/j.entcs.2004.05.020","article-title":"Metareasoning about security protocols using distributed temporal logic","volume":"125","author":"Caleiro","year":"2005","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2024051714215170300_ref10","doi-asserted-by":"crossref","first-page":"637","DOI":"10.1093\/jigpal\/jzi048","article-title":"Relating strand spaces and distributed temporal logic for security protocol analysis","volume":"13","author":"Caleiro","year":"2005","journal-title":"Logic Journal of the IGPL"},{"key":"2024051714215170300_ref11","article-title":"Characterizing correctness properties of parallel programs using fixpoints","volume-title":"Automata, Languages and Programming. ICALP 1980","author":"Clarke","year":"1980"},{"key":"2024051714215170300_ref12","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0025774","article-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","volume-title":"Logics of Programs","author":"Clarke","year":"1982"},{"key":"2024051714215170300_ref13","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic verification of finite-state concurrent systems using temporal logic specifications","volume":"8","author":"Clarke","year":"1986","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"2024051714215170300_ref14","doi-asserted-by":"crossref","first-page":"591","DOI":"10.1007\/s002360050167","article-title":"Specifying communication in distributed information systems","volume":"36","author":"Ehrich","year":"2000","journal-title":"Acta Informatica"},{"key":"2024051714215170300_ref15","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-1-4615-5643-5_6","article-title":"Logics for specifying concurrent information systems","volume-title":"Logic for Databases and Information Systems","author":"Ehrich","year":"1998"},{"volume-title":"The SPIN Model Checker: Primer and Reference Manual","year":"2004","author":"Holzmann","key":"2024051714215170300_ref16"},{"volume-title":"Temporal Logic and State Systems","year":"2008","author":"Kr\u00f6ger","key":"2024051714215170300_ref17"},{"key":"2024051714215170300_ref18","first-page":"97","article-title":"Checking that finite state concurrent programs satisfy their linear specification","volume-title":"POPL, Proc. 12th ACM Symp.","author":"Lichtenstein","year":"1985"},{"key":"2024051714215170300_ref19","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1093\/jigpal\/8.1.55","article-title":"Propositional temporal logic: Decidability and completeness","volume":"8","author":"Lichtenstein","year":"2000","journal-title":"Logic Journal of the IGPL"},{"key":"2024051714215170300_ref20","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1142\/S0129054192000103","article-title":"Temporal logics for communicating sequential agents: I","volume":"03","author":"Lodaya","year":"1992","journal-title":"International Journal of Foundations of Computer Science"},{"key":"2024051714215170300_ref21","first-page":"290","article-title":"A modal logic for a subclass of event structures","volume-title":"Proceedings of 14th ICALP","author":"Lodaya","year":"1987"},{"key":"2024051714215170300_ref22","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"McMillan","year":"1993"},{"key":"2024051714215170300_ref23","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1142\/9789814271059_0009","article-title":"Automata on distributed alphabets","volume-title":"Modern Applications of Automata Theory","author":"Mukund","year":"2012"},{"key":"2024051714215170300_ref24","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/11559306_7","article-title":"A complete temporal and spatial logic for distributed systems","volume-title":"Frontiers of Combining Systems","author":"Pattinson","year":"2005"},{"key":"2024051714215170300_ref25","first-page":"46","article-title":"The temporal logic of programs","volume-title":"FOCS","author":"Pnueli","year":"1977"},{"key":"2024051714215170300_ref26","first-page":"118","article-title":"Locally linear time temporal logic","volume-title":"Proceeding of 11th LICS","author":"Ramanujam","year":"1996"},{"key":"2024051714215170300_ref27","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":"Computer Science Review"},{"volume-title":"Distributed Systems: Principles and Paradigms","year":"2006","author":"Tanenbaum","key":"2024051714215170300_ref28"},{"key":"2024051714215170300_ref29","doi-asserted-by":"crossref","first-page":"643","DOI":"10.1007\/3-540-65306-6_24","article-title":"Distributed versions of linear time temporal logic: A trace perspective","volume-title":"Lectures on Petri Nets I: Basic Models: Advances in Petri Nets","author":"Thiagarajan","year":"1998"},{"key":"2024051714215170300_ref30","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1007\/978-3-540-69850-0_10","article-title":"From church and prior to PSL","volume-title":"Proceedings of Workshop on 25 Years of Model Checking","author":"Vardi","year":"2008"},{"key":"2024051714215170300_ref31","first-page":"332","article-title":"An automata-theoretic approach to automatic program verification","volume-title":"Proc. of 1st LICS","author":"Vardi","year":"1986"},{"key":"2024051714215170300_ref32","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","article-title":"Reasoning about infinite computations","volume":"115","author":"Vardi","year":"1994","journal-title":"Information and Computation"},{"key":"2024051714215170300_ref33","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/3-540-17906-2_31","article-title":"Event structures","volume-title":"Petri Nets: Applications and Relationships to Other Models of Concurrency, LNCS 255","author":"Winskel","year":"1987"}],"container-title":["Logic Journal of the IGPL"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/jigpal\/advance-article-pdf\/doi\/10.1093\/jigpal\/jzae043\/57697325\/jzae043.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/jigpal\/advance-article-pdf\/doi\/10.1093\/jigpal\/jzae043\/57697325\/jzae043.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,17]],"date-time":"2024-05-17T15:00:49Z","timestamp":1715958049000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/jigpal\/advance-article\/doi\/10.1093\/jigpal\/jzae043\/7664678"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,16]]},"references-count":33,"URL":"https:\/\/doi.org\/10.1093\/jigpal\/jzae043","relation":{},"ISSN":["1367-0751","1368-9894"],"issn-type":[{"type":"print","value":"1367-0751"},{"type":"electronic","value":"1368-9894"}],"subject":[],"published":{"date-parts":[[2024,5,16]]},"article-number":"jzae043"}}