{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,30]],"date-time":"2023-01-30T23:53:18Z","timestamp":1675122798176},"reference-count":43,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2010,2,26]],"date-time":"2010-02-26T00:00:00Z","timestamp":1267142400000},"content-version":"unspecified","delay-in-days":25,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2010,2]]},"abstract":"<jats:p>Modal and mixed transition systems are specification formalisms that allow the mixing of over- and under-approximation. We discuss three fundamental decision problems for such specifications:\n<jats:list list-type=\"bullet\"><jats:list-item><jats:label>\u2014<\/jats:label><jats:p>whether a set of specifications has a common implementation;<\/jats:p><\/jats:list-item><jats:list-item><jats:label>\u2014<\/jats:label><jats:p>whether an individual specification has an implementation; and<\/jats:p><\/jats:list-item><jats:list-item><jats:label>\u2014<\/jats:label><jats:p>whether all implementations of an individual specification are implementations of another one.<\/jats:p><\/jats:list-item><\/jats:list>\nFor each of these decision problems we investigate the worst-case computational complexity for the modal and mixed cases. We show that the first decision problem is EXPTIME-complete for both modal and mixed specifications. We prove that the second decision problem is EXPTIME-complete for mixed specifications (it is known to be trivial for modal ones). The third decision problem is also shown to be EXPTIME-complete for mixed specifications.<\/jats:p>","DOI":"10.1017\/s0960129509990260","type":"journal-article","created":{"date-parts":[[2010,2,26]],"date-time":"2010-02-26T10:29:58Z","timestamp":1267180198000},"page":"75-103","source":"Crossref","is-referenced-by-count":5,"title":["Modal and mixed specifications: key decision problems and their complexities"],"prefix":"10.1017","volume":"20","author":[{"given":"ADAM","family":"ANTONIK","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"MICHAEL","family":"HUTH","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"KIM G.","family":"LARSEN","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ULRIK","family":"NYMAN","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ANDRZEJ","family":"W\u0104SOWSKI","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2010,2,26]]},"reference":[{"key":"S0960129509990260_ref41","article-title":"Alternating tree automata, parity games, and modal \u03bc-calculus","volume":"8","author":"Wilke","year":"2001","journal-title":"Bull. Soc. Math. Belg."},{"key":"S0960129509990260_ref39","doi-asserted-by":"crossref","DOI":"10.1145\/230514.571645","volume-title":"Introduction to the Theory of Computation","author":"Sipser","year":"1996"},{"key":"S0960129509990260_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0017309"},{"key":"S0960129509990260_ref33","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1990.113738"},{"key":"S0960129509990260_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60630-0_2"},{"key":"S0960129509990260_ref30","doi-asserted-by":"crossref","unstructured":"Larsen K. G. , Nyman U. and W\u0105sowski A. (2007b) On modal refinement and consistency. In: Caires L. and Vasconcelos V. T. (eds.) CONCUR 2007. Springer-Verlag Lecture Notes in Computer Science 4703 105\u2013119.","DOI":"10.1007\/978-3-540-74407-8_8"},{"key":"S0960129509990260_ref29","doi-asserted-by":"crossref","unstructured":"Larsen K. G. , Nyman U. and W\u0105sowski A. (2007a) Modal I\/O automata for interface and product line theories. In: Nicola R. D. (ed.) ESOP. Springer-Verlag Lecture Notes in Computer Science 4421 64\u201379.","DOI":"10.1007\/978-3-540-71316-6_6"},{"key":"S0960129509990260_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(63)90169-4"},{"key":"S0960129509990260_ref24","unstructured":"H\u00fcttel H. (1988) Operational and denotational properties of modal process logic. Master's thesis, Computer Science Department, Aalborg University."},{"key":"S0960129509990260_ref21","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-1(1:1)2005"},{"key":"S0960129509990260_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_18"},{"key":"S0960129509990260_ref43","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00009-7"},{"key":"S0960129509990260_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44685-0_29"},{"key":"S0960129509990260_ref18","first-page":"158","volume-title":"Proceedings of the Twentieth Annual IEEE Symp. on Logic in Computer Science, LICS 2005","author":"Godefroid","year":"2005"},{"key":"S0960129509990260_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/1147249.1147254"},{"key":"S0960129509990260_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"S0960129509990260_ref14","first-page":"341","article-title":"La totalit\u00e9 des nombres premiers inf\u00e9rieurs a une limite donn\u00e9e","volume":"17","author":"Chebyshev","year":"1852","journal-title":"Journal de Mathematiques Pures et Appliques"},{"key":"S0960129509990260_ref12","doi-asserted-by":"crossref","unstructured":"Bruns G. and Godefroid P. (2000) Generalized model checking: Reasoning about partial state spaces. In: Palamidessi C. (ed.) CONCUR. Springer-Verlag Lecture Notes in Computer Science 1877 168\u2013182.","DOI":"10.1007\/3-540-44618-4_14"},{"key":"S0960129509990260_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(96)00027-5"},{"key":"S0960129509990260_ref10","doi-asserted-by":"crossref","unstructured":"Brunet G. , Chechik M. and Uchitel S. (2006) Properties of behavioural model merging. In: Misra J. , Nipkow T. and Sekerinski E. (eds.) FM. Springer-Verlag Lecture Notes in Computer Science 4085 98\u2013114.","DOI":"10.1007\/11813040_8"},{"key":"S0960129509990260_ref9","unstructured":"B\u00f8rjesson A. , Larsen K. G. and Skou A. (1993) Generality in design and compositional verification using tav. In: FORTE '92 Proceedings, North-Holland Publishing Co. 449\u2013464."},{"key":"S0960129509990260_ref28","doi-asserted-by":"crossref","unstructured":"Larsen K. G. (1989) Modal specifications. In Sifakis J. (ed.) Automatic Verification Methods for Finite State Systems. Springer-Verlag Lecture Notes in Computer Science 407 232\u2013246.","DOI":"10.1007\/3-540-52148-8_19"},{"key":"S0960129509990260_ref8","unstructured":"Berwanger D. and Doyen L. (2008) On the power of imperfect information. In: Proceedings of the 28th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'08), Bangalore, India, December 2008. Available at http:\/\/drops.dagstuhl.de\/portals\/FSTTCS08\/."},{"key":"S0960129509990260_ref42","unstructured":"Xinxin L. (1992) Specification and Decomposition in Concurrency, Ph.D. thesis, Department of Mathematics and Comnputer Science, Aalborg University."},{"key":"S0960129509990260_ref23","doi-asserted-by":"crossref","unstructured":"Huth M. , Jagadeesan R. and Schmidt D. (2001) Modal transition systems: A foundation for three-valued program analysis. Springer-Verlag Lecture Notes in Computer Science 2028.","DOI":"10.1007\/3-540-45309-1_11"},{"key":"S0960129509990260_ref16","unstructured":"Dams D. (1996) Abstract Interpretation and Partition Refinement for Model Checking, Ph.D. thesis, Eindhoven University of Technology."},{"key":"S0960129509990260_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/BF00370554"},{"key":"S0960129509990260_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_27"},{"key":"S0960129509990260_ref37","unstructured":"Schmidt D. (2001) From trace sets to modal-transition systems by stepwise abstract interpretation."},{"key":"S0960129509990260_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-005-0063-z"},{"key":"S0960129509990260_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2007.01.003"},{"key":"S0960129509990260_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"key":"S0960129509990260_ref34","unstructured":"Nyman U. (2008) Modal Transition Systems as the Basis for Interface Theories and Product Lines, Ph.D. thesis, Department of Computer Science, Aalborg University."},{"key":"S0960129509990260_ref32","first-page":"203","volume-title":"Third Annual IEEE Symposium on Logic in Computer Science (LICS)","author":"Larsen","year":"1988"},{"key":"S0960129509990260_ref36","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.06.023"},{"key":"S0960129509990260_ref3","unstructured":"Antonik A. , Huth M. , Larsen K. G. , Nyman U. and W\u0105sowski A. (2008a) 20 years of modal and mixed specifications. Bulletin of EATCS 95. (Available at http:\/\/processalgebra.blogspot.com\/2008\/05\/concurrency-column-for-beatcs-june-2008.html.)"},{"key":"S0960129509990260_ref38","unstructured":"Schmidt H. and Fecher H. (2007) Comparing disjunctive modal transition systems with a one-selecting variant. (Submitted for publication.)"},{"key":"S0960129509990260_ref40","doi-asserted-by":"publisher","DOI":"10.1145\/1041685.1029904"},{"key":"S0960129509990260_ref1","unstructured":"Antonik A. (2008) Decision problems for partial specifications: empirical and worst-case complexity, Ph.D. thesis, Imperial College, London."},{"key":"S0960129509990260_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_9"},{"key":"S0960129509990260_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.08.002"},{"key":"S0960129509990260_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.06.011"},{"key":"S0960129509990260_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03466-4_7"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129509990260","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T20:56:17Z","timestamp":1556484977000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129509990260\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,2]]},"references-count":43,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,2]]}},"alternative-id":["S0960129509990260"],"URL":"https:\/\/doi.org\/10.1017\/s0960129509990260","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,2]]}}}