================================================================================
P9309   J.C.M. Baeten, J.A. Bergstra & R.N. Bol
        "A real time process logic"


Systems can be described at various levels of abstraction: automata,
processes and behavior. In this paper, we take the ready trace set as a
description of the behavior of a process, and we present a ready trace
model of symbolic (untimed) and real time process algebra. We argue that,
especially in the real time case, properties of ready trace sets are best
formulated in a dedicated logic (as opposed to describing them in an
enriched process notation, such as ACP-tau). We present the syntax and
semantics of a logic that could serve this purpose, and we apply it on two
examples: expressing the correctness of a concurrent alternating bit
protocol, and demonstrating the (well-known) non-existence of so-called
coordinated attack protocols. A connection is made with the metric temporal
logic of Koymans.



@inproceedings{P9309,
        author =        {J.C.M. Baeten and J.A. Bergstra and R.N. Bol},
        title =         {A real time process logic},
        pages =         {},
        booktitle =     {Proceedings ICTL'94},
        place =		{Bonn},
        year =          {1994},
        editor =        {},
        series =        {LNCS},
        volume =        {},
        publisher =     {Springer}
}

[
J.C.M. Baeten, J.A. Bergstra & R.N. Bol, A real time process logic, Progr.
report P9309, UvA 1993, report CSN 93/15, EUT 1993. To appear in Proc.
ICTL'94, Bonn 1994, LNCS.
]