Jørgen H. Andersen
Kåre J. Kristoffersen
Kim G. Larsen
Jesper Niedermann
In 6th NWPT, pages 448-464
where is a
real time (logical) specification,
are given (regular) timed
agents and the problem is to decide whether there exists (and if possible
exhibit) a real time agent
which when put in parallel with
will yield a network satisfying
. The method presented proceeds in
two steps: first, the implicit specification of
is transformed into an
equivalent direct specification of
; second, a model for this direct
specification is constructed (if possible) using a direct model construction
algorithm. A prototype implementation of our method has been added to the
real time verification tool EPSILON.
Comments
BRICS, Department of Math. & Comp. Sc., Aalborg
University.
Available as PostScript.