LOTOS enhancement to specify time constraint among 
non-adjacent actions using first order logic

Akio Nakata, Teruo Higashino and Kenichi Taniguchi
Department of Information and Computer Science, Osaka University

E-mail:{nakata,higashino,taniguchi}@ics.es.osaka-u.ac.jp

Abstract

In this paper, we propose
a language LOTOS/T, which is an enhancement of Basic LOTOS.
LOTOS/T enables us to describe time constraints in formulas 
of 1st-order predicate logic.
The user only describes the logical
relation of time at which each action must be executed.
Use of equality ($=$) and inequality ($\le$) as the time constraints
enables us to describe intervals, timeout and delay easily.
We define the syntax and semantics of LOTOS/T formally.
The semantic model of LOTOS/T is the Labelled Transition System (LTS).
We give the inference rules for constructing the LTS's from given LOTOS/T
expressions.
The LTS's can be constructed mechanically.
Then, we show how flexible and convenient to specify practical
real-time systems in LOTOS/T with an example.  
We also define both timed and untimed bisimulation equivalences
and give a method to verify their equivalences mechanically.