{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T14:44:18Z","timestamp":1749825858229,"version":"3.38.0"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,1,4]],"date-time":"2012-01-04T00:00:00Z","timestamp":1325635200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2012,4]]},"DOI":"10.1007\/s10703-011-0138-9","type":"journal-article","created":{"date-parts":[[2012,1,3]],"date-time":"2012-01-03T13:12:33Z","timestamp":1325596353000},"page":"263-281","source":"Crossref","is-referenced-by-count":7,"title":["Achieving distributed control through model checking"],"prefix":"10.1007","volume":"40","author":[{"given":"Susanne","family":"Graf","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sophie","family":"Quinton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,1,4]]},"reference":[{"key":"138_CR1","series-title":"LNCS","first-page":"79","volume-title":"Proceedings of CAV\u201909","author":"A Basu","year":"2009","unstructured":"Basu A, Bensalem S, Peled D, Sifakis J (2009) Priority scheduling of distributed systems based on model checking. In: Proceedings of CAV\u201909. LNCS, vol 5643. Springer, Berlin, pp 79\u201393"},{"key":"138_CR2","series-title":"LNCS","first-page":"52","volume-title":"Proceedings of ATVA\u201910","author":"S Bensalem","year":"2010","unstructured":"Bensalem S, Bozga M, Graf S, Peled D, Quinton S (2010) Methods for knowledge-based controlling of distributed systems. In: Proceedings of ATVA\u201910. LNCS, vol 6252. Springer, Berlin, pp 52\u201366"},{"key":"138_CR3","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning about knowledge","author":"R Fagin","year":"1995","unstructured":"Fagin R, Halpern JY, Vardi MY, Moses Y (1995) Reasoning about knowledge. MIT Press, Cambridge"},{"key":"138_CR4","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/0304-3975(81)90113-4","volume":"13","author":"HJ Genrich","year":"1981","unstructured":"Genrich HJ, Lautenbach K (1981) System modelling with high-level petri nets. Theor Comput Sci 13:109\u2013136","journal-title":"Theor Comput Sci"},{"key":"138_CR5","series-title":"LNCS","first-page":"435","volume-title":"Proceedings of TACAS\u201910","author":"G Katz","year":"2010","unstructured":"Katz G, Peled D (2010) Code mutation in verification and automatic code correction. In: Proceedings of TACAS\u201910. LNCS, vol 6015. Springer, Berlin, pp 435\u2013450"},{"key":"138_CR6","series-title":"LNCS","first-page":"510","volume-title":"Proceedings of CAV\u201911","author":"G Katz","year":"2011","unstructured":"Katz G, Peled D, Schewe S (2011) Synthesis of Distributed Control through Knowledge Accumulation. In: Proceedings of CAV\u201911. LNCS, vol 6807. Springer, Berlin, pp 510\u2013525"},{"issue":"7","key":"138_CR7","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1145\/360248.360251","volume":"19","author":"RM Keller","year":"1976","unstructured":"Keller RM (1976) Formal verification of parallel programs. Commun ACM 19(7):371\u2013384","journal-title":"Commun ACM"},{"issue":"2","key":"138_CR8","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1006\/inco.1997.2679","volume":"140","author":"R Meyden van\u00a0der","year":"1998","unstructured":"van\u00a0der Meyden R (1998) Common knowledge and update in finite environment. Inf Comput 140(2):115\u2013157","journal-title":"Inf Comput"},{"issue":"5","key":"138_CR9","doi-asserted-by":"crossref","first-page":"406","DOI":"10.1016\/1385-7258(77)90055-5","volume":"80","author":"JB Orlin","year":"1977","unstructured":"Orlin JB (1977) Contentment in graph theory: covering graphs with cliques. Indag Math 80(5):406\u2013424","journal-title":"Indag Math"},{"issue":"12","key":"138_CR10","doi-asserted-by":"crossref","first-page":"1173","DOI":"10.1002\/cpe.903","volume":"16","author":"JA P\u00e9rez","year":"2004","unstructured":"P\u00e9rez JA, Corchuelo R, Toro M (2004) An order-based algorithm for implementing multiparty synchronization. Concurr Pract Exp 16(12):1173\u20131206","journal-title":"Concurr Pract Exp"},{"issue":"9","key":"138_CR11","doi-asserted-by":"crossref","first-page":"1656","DOI":"10.1109\/9.880616","volume":"45","author":"K Rudie","year":"2000","unstructured":"Rudie K, Ricker SL (2000) Know means no: Incorporating knowledge into discrete-event control systems. IEEE Trans Autom Control 45(9):1656\u20131668","journal-title":"IEEE Trans Autom Control"},{"issue":"11","key":"138_CR12","doi-asserted-by":"crossref","first-page":"1692","DOI":"10.1109\/9.173140","volume":"37","author":"K Rudie","year":"1992","unstructured":"Rudie K, Wonham WM (1992) Think globally, act locally: decentralized supervisory control. IEEE Trans Autom Control 37(11):1692\u20131708","journal-title":"IEEE Trans Autom Control"},{"key":"138_CR13","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1016\/j.sysconle.2004.10.002","volume":"54","author":"JG Thistle","year":"2005","unstructured":"Thistle JG (2005) Undecidability in decentralized supervision. Syst Control Lett 54:503\u2013509","journal-title":"Syst Control Lett"},{"key":"138_CR14","series-title":"LNCS","first-page":"1","volume-title":"Proceedings of STACS\u201995","author":"W Thomas","year":"1995","unstructured":"Thomas W (1995) On the synthesis of strategies in infinite games. In: Proceedings of STACS\u201995. LNCS, vol 900. Springer, Berlin, pp 1\u201313"},{"issue":"1","key":"138_CR15","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1016\/j.ipl.2004.01.004","volume":"90","author":"S Tripakis","year":"2004","unstructured":"Tripakis S (2004) Undecidable problems of decentralized observation and control on regular languages. Inf Process Lett 90(1):21\u201328","journal-title":"Inf Process Lett"},{"issue":"3","key":"138_CR16","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1023\/A:1015625600613","volume":"12","author":"TS Yoo","year":"2002","unstructured":"Yoo TS, Lafortune S (2002) A general architecture for decentralized supervisory control of discrete-event systems. Discret Event Dyn Syst 12(3):335\u2013377","journal-title":"Discret Event Dyn Syst"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0138-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-011-0138-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0138-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,17]],"date-time":"2025-03-17T12:30:28Z","timestamp":1742214628000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-011-0138-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1,4]]},"references-count":16,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["138"],"URL":"https:\/\/doi.org\/10.1007\/s10703-011-0138-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2012,1,4]]}}}