Brandin, Bertil A.Malik, RobiMalik, Petra2008-11-112008-11-112004Brandin, B., Malik, R. & Malik, P. (2004). Incremental verification and synthesis of discrete-event systems guided by counter-examples. IEEE Transactions on Control Systems Technology, 12(3), 387-401.1063-6536https://hdl.handle.net/10289/1300This article presents new approaches to system verification and synthesis based on subsystem verification and the novel combined use of counterexamples and heuristics to identify suitable subsystems incrementally. The scope of safety properties considered is limited to behavioral inclusion and controllability. The verification examples considered provide a comparison of the approaches presented with straightforward state exploration and an understanding of their applicability in an industrial context.application/pdfenCopyright IEEE 2004computer scienceheuristic methodbehavioral analysiscontrollabilitydiscrete event systemprogram verificationJournal Article10.1109/TCST.2004.824795