Analysis and synthesis procedures of discrete event systems in a temporal logic framework

Author

Lin, Jing-Yue ; Ionescu, Dan

Author_Institution

Dept. of Electr. Eng., Ottawa Univ., Ont., Canada

fYear

1992

fDate

11-13 Aug 1992

Firstpage

184

Lastpage

191

Abstract

A model, based on event structures, a set of temporal logic formulas, an initial state, and a labeling function, for the characterization of discrete event systems (DES) is proposed and used for the investigation of system properties such as verification and reachability. For the synthesis procedure, as applied to DES, a composition rule of 2 systems is developed, and a controller design procedure is introduced. An example of a computer file system is used to illustrate this approach

Keywords

control system analysis; control system synthesis; controllability; discrete event simulation; temporal logic; computer file system; controller design procedure; discrete event system analysis; discrete event system synthesis; discrete event systems; labeling function; reachability; temporal logic framework; verification; Computer science; Control system synthesis; Control systems; Discrete event systems; File systems; Labeling; Logic; Operating systems; Reachability analysis; Real time systems;

fLanguage

English

Publisher

ieee

Conference_Titel

Intelligent Control, 1992., Proceedings of the 1992 IEEE International Symposium on

Conference_Location

Glasgow

ISSN

2158-9860

Print_ISBN

0-7803-0546-9

Type

conf

DOI

10.1109/ISIC.1992.225089

Filename

225089

Link To Document

https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3222602