{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:04:06Z","timestamp":1773655446720,"version":"3.50.1"},"reference-count":24,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"3","license":[{"start":{"date-parts":[[2004,5,1]],"date-time":"2004-05-01T00:00:00Z","timestamp":1083369600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Contr. Syst. Technol."],"published-print":{"date-parts":[[2004,5]]},"DOI":"10.1109\/tcst.2004.824795","type":"journal-article","created":{"date-parts":[[2004,5,6]],"date-time":"2004-05-06T17:08:33Z","timestamp":1083863313000},"page":"387-401","source":"Crossref","is-referenced-by-count":53,"title":["Incremental Verification and Synthesis of Discrete-Event Systems Guided by Counter Examples"],"prefix":"10.1109","volume":"12","author":[{"given":"B.A.","family":"Brandin","sequence":"first","affiliation":[]},{"given":"R.","family":"Malik","sequence":"additional","affiliation":[]},{"given":"P.","family":"Malik","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-3227-1_8","article-title":"Synchronous observers and the verification of reactive systems","volume-title":"Proc. 3rd Int. Conf. Algebraic Methodology and Software Technology","author":"Halbwachs"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1995.480192"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/226295.226321"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/5.21072"},{"key":"ref5","volume-title":"Notes on Control of Discrete Event Systems","author":"Wonham","year":"1999"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/BF02551233"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4070-7"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/acc.2000.876984"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.3182\/20020721-6-es-1901.00517"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/322123.322134"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/357980.358021"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1137\/0325036"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"ref14","volume-title":"Projekt BMW E65 CAS\u2014FH-Master\u2014Eine Modellierung in DCD","author":"Dietrich","year":"2000"},{"key":"ref15","volume-title":"From Supervisory Control to Nonblocking Controllers for Discrete Event Systems","author":"Malik","year":"2003"},{"key":"ref16","volume-title":"Case Study \u201cProduction Cell\u201d","volume":"891","author":"Lewerentz","year":"1995"},{"key":"ref17","volume-title":"Task Description of a Flexible Production Cell With Real Time Properties","author":"L\u00f6tzbeyer","year":"1996"},{"issue":"2","key":"ref18","first-page":"138","article-title":"A case study in verification of UML statecharts: the PROFIsafe protocol","volume":"9","author":"Malik","year":"2003","journal-title":"J. Universal Comput. Sci."},{"key":"ref19","volume-title":"Testing the PROFIsafe Protocol Using Automatically Generated Test Cases Based on a Formally Verified Model","author":"Malik","year":"2002"},{"key":"ref20","year":"2002","journal-title":"PROFIsafe-Profile for Safety Technology, Version 1.12"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/CIMAT.1994.389054"},{"key":"ref22","volume-title":"Commande par Supervision des Syst\u00e8mes \u00e0 \u00c9v\u00e9nements Discrets: Application \u00e0 un Site Exp\u00e9rimental l\u2019Atelier Inter-\u00c9tablissement de Productique","author":"Charbonnier","year":"1994"},{"key":"ref23","volume-title":"Hierarchical Interface-Based Supervisory Control","author":"Leduc","year":"2002"},{"key":"ref24","volume-title":"PLC Implementation of a DES Supervisor for a Manufacturing Testbed: An Implementation Perspective","author":"Leduc","year":"1996"}],"container-title":["IEEE Transactions on Control Systems Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/87\/28760\/01291409.pdf?arnumber=1291409","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,21]],"date-time":"2025-04-21T04:14:36Z","timestamp":1745208876000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1291409\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,5]]},"references-count":24,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2004,5]]}},"URL":"https:\/\/doi.org\/10.1109\/tcst.2004.824795","relation":{},"ISSN":["1063-6536"],"issn-type":[{"value":"1063-6536","type":"print"}],"subject":[],"published":{"date-parts":[[2004,5]]}}}