{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,10]],"date-time":"2024-07-10T15:30:16Z","timestamp":1720625416222},"reference-count":32,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2013,8,1]],"date-time":"2013-08-01T00:00:00Z","timestamp":1375315200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,12]],"date-time":"2013-08-12T00:00:00Z","timestamp":1376265600000},"content-version":"vor","delay-in-days":11,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2013,8]]},"DOI":"10.1016\/j.entcs.2013.07.011","type":"journal-article","created":{"date-parts":[[2013,8,12]],"date-time":"2013-08-12T21:05:25Z","timestamp":1376341525000},"page":"163-181","source":"Crossref","is-referenced-by-count":1,"special_numbering":"C","title":["Extending a Synthesis-Centric Model-Based Systems Engineering Framework with Stochastic Model Checking"],"prefix":"10.1016","volume":"296","author":[{"given":"J.","family":"Markovski","sequence":"first","affiliation":[]},{"given":"E.S.","family":"Estens Musa","sequence":"additional","affiliation":[]},{"given":"M.A.","family":"Reniers","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.entcs.2013.07.011_br0010","series-title":"Proceedings of WODES 2006","first-page":"384","article-title":"Supremica - an integrated environment for verification, synthesis and simulation of discrete event systems","author":"Akesson","year":"2006"},{"key":"10.1016\/j.entcs.2013.07.011_br0020","series-title":"Proceedings of IFIP TCS 2004","first-page":"493","article-title":"Controller synthesis for probabilistic systems","author":"Baier","year":"2004"},{"key":"10.1016\/j.entcs.2013.07.011_br0030","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","article-title":"Model-checking algorithms for continuous-time Markov chains","volume":"29","author":"Baier","year":"2003","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/j.entcs.2013.07.011_br0040","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1145\/1059816.1059819","article-title":"Model checking meets performance evaluation","volume":"32","author":"Baier","year":"2005","journal-title":"SIGMETRICS Performance Evaluation Review"},{"key":"10.1016\/j.entcs.2013.07.011_br0050","series-title":"Automata, Languages and Programming","first-page":"148","article-title":"Controller synthesis and verification for Markov decision processes with qualitative branching time objectives","volume":"vol. 5126","author":"Br\u00e1zdil","year":"2010"},{"key":"10.1016\/j.entcs.2013.07.011_br0060","series-title":"Introduction to discrete event systems","author":"Cassandras","year":"2004"},{"key":"10.1016\/j.entcs.2013.07.011_br0070","series-title":"Computer Science Logic","first-page":"100","article-title":"Simple stochastic parity games","volume":"vol. 2803","author":"Chatterjee","year":"2003"},{"key":"10.1016\/j.entcs.2013.07.011_br0080","series-title":"Fuzzy Systems and Knowledge Discovery","first-page":"149","article-title":"On the Markovian randomized strategy of controller for Markov decision processes","volume":"vol. 4223","author":"Chen","year":"2006"},{"key":"10.1016\/j.entcs.2013.07.011_br0090","series-title":"Verification of Stochastic Requirements in Supervised Plants","author":"Estens Musa","year":"2012"},{"key":"10.1016\/j.entcs.2013.07.011_br0100","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1109\/9.746254","article-title":"A probabilistic language formalism for stochastic discrete-event systems","volume":"44","author":"Garg","year":"1999","journal-title":"IEEE Transactions on Automatic Control"},{"key":"10.1016\/j.entcs.2013.07.011_br0110","article-title":"Interactive Markov Chains and the Quest For Quantified Quantity","volume":"vol. 2428","author":"Hermanns","year":"2002"},{"key":"10.1016\/j.entcs.2013.07.011_br0120","series-title":"Proceedings of MMB 2008","first-page":"1","article-title":"May we reach it? or must we? in what time? with what probability?","author":"Hermanns","year":"2008"},{"key":"10.1016\/j.entcs.2013.07.011_br0130","series-title":"Dynamic Probabilistic Systems","author":"Howard","year":"1971"},{"key":"10.1016\/j.entcs.2013.07.011_br0140","series-title":"Proceedings of QEST 2005","first-page":"243","article-title":"A Markov reward model checker","author":"Katoen","year":"2005"},{"key":"10.1016\/j.entcs.2013.07.011_br0150","series-title":"Proceedings of CDC 1998","first-page":"3299","article-title":"Control of stochastic discrete event systems: Synthesis","author":"Kumar","year":"1998"},{"key":"10.1016\/j.entcs.2013.07.011_br0160","series-title":"Feedback Control, Nonlinear Systems, and Complexity","first-page":"114","article-title":"Performance analysis and control of stochastic discrete event systems","volume":"vol. 202","author":"Kwong","year":"1995"},{"key":"10.1016\/j.entcs.2013.07.011_br0170","first-page":"327","article-title":"Supervisory control of probabilistic discrete event systems","volume":"vol. 1","author":"Lawford","year":"1993"},{"key":"10.1016\/j.entcs.2013.07.011_br0180","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1109\/52.60589","article-title":"The challenge of building process-control software","volume":"7","author":"Leveson","year":"1990","journal-title":"IEEE Software"},{"key":"10.1016\/j.entcs.2013.07.011_br0190","series-title":"Logistic Optimization of Chemical Production Processes","first-page":"37","article-title":"Logistic simulation of pipeless plants","author":"Liefeldt","year":"2008"},{"key":"10.1016\/j.entcs.2013.07.011_br0200","series-title":"Proceedings of PSE 2003, Computer-Aided Chemical Engineering 15","first-page":"956","article-title":"A modelling and simulation environment for pipeless plants","author":"Liefeldt","year":"2003"},{"key":"10.1016\/j.entcs.2013.07.011_br0210","series-title":"Proceedings of ACSD 2011","first-page":"108","article-title":"Towards supervisory control of Interactive Markov chains: Controllability","author":"Markovski","year":"2011"},{"key":"10.1016\/j.entcs.2013.07.011_br0220","series-title":"Proceedings of CASE 2012","article-title":"A process-theoretic state-based framework for live supervision","author":"Markovski","year":"2012"},{"key":"10.1016\/j.entcs.2013.07.011_br0230","series-title":"Proceedings of ETFA 2012","article-title":"Process theory for supervisory control of stochastic systems with data","author":"Markovski","year":"2012"},{"key":"10.1016\/j.entcs.2013.07.011_br0240","author":"Markovski"},{"key":"10.1016\/j.entcs.2013.07.011_br0250","series-title":"Proceedings of ACSD 2012","first-page":"52","article-title":"Verifying performance of supervised plants","author":"Markovski","year":"2012"},{"key":"10.1016\/j.entcs.2013.07.011_br0260","series-title":"Proceedings of CDC 2010","first-page":"3481","article-title":"A state-based framework for supervisory control synthesis and verification","author":"Markovski","year":"2010"},{"key":"10.1016\/j.entcs.2013.07.011_br0270","series-title":"Proceedings of WODES 2008","first-page":"193","article-title":"Extraction and representation of a supervisor using guards in extended finite automata","author":"Miremadi","year":"2008"},{"key":"10.1016\/j.entcs.2013.07.011_br0280","doi-asserted-by":"crossref","first-page":"2013","DOI":"10.1109\/TAC.2009.2024376","article-title":"Probabilistic supervisory control of probabilistic discrete event systems","volume":"54","author":"Pantelic","year":"2009","journal-title":"IEEE Transactions on Automatic Control"},{"key":"10.1016\/j.entcs.2013.07.011_br0290","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1137\/0325013","article-title":"Supervisory control of a class of discrete-event processes","volume":"25","author":"Ramadge","year":"1987","journal-title":"SIAM Journal on Control and Optimization"},{"key":"10.1016\/j.entcs.2013.07.011_br0300","first-page":"1","article-title":"Model-based engineering of supervisory controllers using CIF","volume":"21","author":"Schiffelers","year":"2009","journal-title":"Electronic Communications of the EASST"},{"key":"10.1016\/j.entcs.2013.07.011_br0310","series-title":"Proc. 2012 IEEE Multiconference on System and Control","article-title":"Timed automata based scheduling for a miniature pipeless plant with mobile robots","author":"Schoppmeyer","year":"2012"},{"key":"10.1016\/j.entcs.2013.07.011_br0320","series-title":"Proceedings of CDC 2007","first-page":"3387","article-title":"Modeling of discrete event systems using finite automata with variables","author":"Skoldstam","year":"2007"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106611300042X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106611300042X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,10,14]],"date-time":"2018-10-14T01:52:32Z","timestamp":1539481952000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S157106611300042X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,8]]},"references-count":32,"alternative-id":["S157106611300042X"],"URL":"https:\/\/doi.org\/10.1016\/j.entcs.2013.07.011","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2013,8]]}}}