×

Synthesizing processes and schedulers from temporal specifications. (English) Zbl 0765.68148

Computer-aided verification, Proc. 2nd Int. Conf., CAV ’90, New Brunswick/NJ (USA), Lect. Notes Comput. Sci. 531, 272-281 (1991).
Summary: [For the entire collection see Zbl 0756.00006.]
We examine two closely related problems: synthesizing processes to satisfy temporal specifications of reactive systems, and the synthesis of a scheduler to interact with and control a group of processes in order to meet a specification. Processes communicate through shared and distributed variables, either synchronously or asynchronously. In the finite state case, processes, and specifications are arbitrary \(\omega\)- regular languages, and both synthesis problems are solvable in doubly exponential time and space. The framework we present is flexible enough to incorporate dense real time into the model of concurrency, thereby allowing us to study the synthesis of real-time processes and schedulers. Real-time implementability and scheduling are also doubly exponential.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)

Citations:

Zbl 0756.00006
PDFBibTeX XMLCite