TY  - JOUR
TI  - Control synthesis for parametric timed automata under reachability
AB  - Timed automata is a fundamental modeling formalism for real-time systems. During the design of such
real-time systems, often the system information is incomplete, and design choices can vary. These uncertainties can
be integrated to the model via parameters and labelled transitions. Then, the design can be completed by tuning the
parameters and restricting the transitions via controller synthesis. These problems, namely parameter synthesis and
controller synthesis, are studied separately in the literature. Herein, these are combined to generate an automaton
satisfying the given specification by both parameter tuning and controller synthesis, thus exploring all design choices.
First, it is shown that the negative decidability results derived for the parameter synthesis problem apply to the proposed
problem. Then, a specific version of the problem is studied, where the specification is to reach a target set and
parameters can take values from bounded integer sets. An algorithm based on depth first analysis combined with
an iterative feasibility check is presented to solve the proposed problem. The correctness and the completeness (under
mild assumptions) of the developed algorithm are proven. The findings of the paper are illustrated on an example drawn
from scheduling.
AU  - AYDIN GOL, EBRU
DO  - 10.3906/elk-2007-170
PY  - 2021
JO  - Turkish Journal of Electrical Engineering and Computer Sciences
VL  - 29
IS  - 3
SN  - 1300-0632
SP  - 1751
EP  - 1764
DB  - TRDizin
UR  - http://search/yayin/detay/523563
ER  -