{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:16:48Z","timestamp":1750306608065,"version":"3.41.0"},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2015,9,9]],"date-time":"2015-09-09T00:00:00Z","timestamp":1441756800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004281","name":"Narodowe Centrum Nauki","doi-asserted-by":"publisher","award":["DEC-2012\/07\/N\/ST6\/03426"],"award-info":[{"award-number":["DEC-2012\/07\/N\/ST6\/03426"]}],"id":[{"id":"10.13039\/501100004281","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2015,12,8]]},"abstract":"<jats:p>The article introduces a parametric extension of Action-Restricted Computation Tree Logic called pmARCTL. A symbolic fixed-point algorithm providing a solution to the exhaustive parameter synthesis problem is proposed. The parametric approach allows for an in-depth system analysis and synthesis of the correct parameter values. The time complexity of the problem and the algorithm is provided. An existential fragment of pmARCTL (pmEARCTL) is identified, in which all of the solutions can be generated from a minimal and unique base. A method for computing this base using symbolic methods is provided. The prototype tool SPATULA implementing the algorithm is applied to the analysis of three benchmarks: faulty Train-Gate-Controller, Peterson\u2019s mutual exclusion protocol, and a generic pipeline processing network. The experimental results show efficiency and scalability of our approach compared to the naive solution to the problem.<\/jats:p>","DOI":"10.1145\/2746337","type":"journal-article","created":{"date-parts":[[2015,9,15]],"date-time":"2015-09-15T12:09:15Z","timestamp":1442318955000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Action Synthesis for Branching Time Logic"],"prefix":"10.1145","volume":"14","author":[{"given":"Micha\u0142","family":"Knapik","sequence":"first","affiliation":[{"name":"Institute of Computer Science, PAS, Warsaw, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Artur","family":"M\u0119ski","sequence":"additional","affiliation":[{"name":"Institute of Computer Science, PAS, Warsaw, and FMCS, University of \u0141\u00f3d\u017a, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wojciech","family":"Penczek","sequence":"additional","affiliation":[{"name":"Institute of Computer Science, PAS, Warsaw, and University of Natural Sciences and Humanities, Siedlce, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,9,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/377978.377990"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/167088.167242"},{"key":"e_1_2_1_3_1","volume-title":"FM 2012: Formal Methods. Lecture Notes in Computer Science","volume":"7436","author":"Fribourg L.","unstructured":"\u00c9. Andr\u00e9, L. Fribourg, U. K\u00fchne, and R. Soulat. 2012. IMITATOR 2.5: A tool for analyzing robustness in scheduling problems. In FM 2012: Formal Methods. Lecture Notes in Computer Science, Vol. 7436. Springer, 33--36."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1373322"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/2361525.2361528"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1342991.1342996"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/648063.747438"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985838"},{"volume-title":"Proceedings of the Synthesis and Simulation Meeting and International Interchange (SASIMI\u201993)","author":"Coudert O.","key":"e_1_2_1_9_1","unstructured":"O. Coudert, J. C. Madre, H. Fraisse, and H. Touati. 1993. Implicit prime cover computation: An overview. In Proceedings of the Synthesis and Simulation Meeting and International Interchange (SASIMI\u201993)."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1137\/070697720"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13089-2_21"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.03.002"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-8326(02)00037-1"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/2343776.2343855"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_36"},{"key":"e_1_2_1_16_1","volume-title":"Simple Parametric Verification Tool. Retrieved","author":"Knapik M.","year":"2014","unstructured":"M. Knapik. 2014. SPATULA, Simple Parametric Verification Tool. Retrieved August 10, 2015, from https:\/\/michalknapik.github.io\/spatula."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2014.22"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74128-2_8"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/647762.735490"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(81)90106-X"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.1952.11988183"},{"volume-title":"Advances in Modal Logic","author":"Schnoebelen P.","key":"e_1_2_1_22_1","unstructured":"P. Schnoebelen. 2002. The complexity of temporal logic model checking. In Advances in Modal Logic, Vol. 4. World Scientific Publishing, 393--436."},{"key":"e_1_2_1_23_1","volume-title":"Retrieved","author":"Somenzi F.","year":"2012","unstructured":"F. Somenzi. 2012. CUDD: CU Decision Diagram Package. Retrieved August 10, 2015, from http:\/\/vlsi.colorado.edu\/&sim;fabio\/CUDD\/cuddIntro.html."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2746337","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2746337","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:16:58Z","timestamp":1750227418000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2746337"}},"subtitle":["Theory and Applications"],"short-title":[],"issued":{"date-parts":[[2015,9,9]]},"references-count":23,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,12,8]]}},"alternative-id":["10.1145\/2746337"],"URL":"https:\/\/doi.org\/10.1145\/2746337","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2015,9,9]]},"assertion":[{"value":"2014-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-03-01","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-09-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}