---
_id: '4637'
abstract:
- lang: eng
text: "In the synchronous composition of processes, one process may prevent another
process from proceeding unless compositions without a well-defined product behavior
are ruled out. They can be ruled out semantically, by insisting on the existence
of certain fixed points, or syntactically, by equipping processes with types,
which make the dependencies between input and output signals transparent. We classify
various typing mechanisms and study their effects on the control problem.\r\nA
static type enforces fixed, acyclic dependencies between input and output ports.
For example, synchronous hardware without combinational loops can be typed statically.
A dynamic type may vary the dependencies from state to state, while maintaining
acyclicity, as in level-sensitive latches. Then, two dynamically typed processes
can be syntactically compatible, if all pairs of possible dependencies are compatible,
or semantically compatible, if in each state the combined dependencies remain
acyclic. For a given plant process and control objective, there may be a controller
of a static type, or only a controller of a syntactically compatible dynamic type,
or only a controller of a semantically compatible dynamic type. We show this to
be a strict hierarchy of possibilities, and we present algorithms and determine
the complexity of the corresponding control problems.\r\nFurthermore, we consider
versions of the control problem in which the type of the controller (static or
dynamic) is given. We show that the solution of these fixed-type control problems
requires the evaluation of partially ordered (Henkin) quantifiers on boolean formulas,
and is therefore harder (nondeterministic exponential time) than more traditional
control questions"
acknowledgement: This research was supported in part by the DARPA grants NAG2-1214
and F33615-C-98-3614, the SRC contract 99-TJ-683.003, the MARCO grant 98-DT-660,
and the NSF CAREER award CCR-9501708.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Luca
full_name: De Alfaro, Luca
last_name: De Alfaro
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Freddy
full_name: Mang, Freddy
last_name: Mang
citation:
ama: 'De Alfaro L, Henzinger TA, Mang F. The control of synchronous systems. In:
Proceedings of the 11th International Conference on Concurrency Theory.
Vol 1877. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2000:458-473. doi:10.1007/3-540-44618-4_33'
apa: 'De Alfaro, L., Henzinger, T. A., & Mang, F. (2000). The control of synchronous
systems. In Proceedings of the 11th International Conference on Concurrency
Theory (Vol. 1877, pp. 458–473). University Park, PA, USA: Schloss Dagstuhl
- Leibniz-Zentrum für Informatik. https://doi.org/10.1007/3-540-44618-4_33'
chicago: De Alfaro, Luca, Thomas A Henzinger, and Freddy Mang. “The Control of Synchronous
Systems.” In Proceedings of the 11th International Conference on Concurrency
Theory, 1877:458–73. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2000.
https://doi.org/10.1007/3-540-44618-4_33.
ieee: L. De Alfaro, T. A. Henzinger, and F. Mang, “The control of synchronous systems,”
in Proceedings of the 11th International Conference on Concurrency Theory,
University Park, PA, USA, 2000, vol. 1877, pp. 458–473.
ista: 'De Alfaro L, Henzinger TA, Mang F. 2000. The control of synchronous systems.
Proceedings of the 11th International Conference on Concurrency Theory. CONCUR:
Concurrency Theory, LNCS, vol. 1877, 458–473.'
mla: De Alfaro, Luca, et al. “The Control of Synchronous Systems.” Proceedings
of the 11th International Conference on Concurrency Theory, vol. 1877, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2000, pp. 458–73, doi:10.1007/3-540-44618-4_33.
short: L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 11th International
Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2000, pp. 458–473.
conference:
end_date: 2000-08-25
location: University Park, PA, USA
name: 'CONCUR: Concurrency Theory'
start_date: 2000-08-22
date_created: 2018-12-11T12:09:53Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-13T11:00:46Z
day: '01'
doi: 10.1007/3-540-44618-4_33
extern: '1'
intvolume: ' 1877'
language:
- iso: eng
month: '01'
oa_version: None
page: 458 - 473
publication: Proceedings of the 11th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783540678977'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '69'
quality_controlled: '1'
status: public
title: The control of synchronous systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1877
year: '2000'
...