🚀 go-pugleaf

I've been using LOTOS as a specification language for concurrent
software and I've run into some issues regarding LOTOS semantics which
I'm not sure I understand. I've been reading the LOTOS standard trying
to figure out the answers, and despite the clarity and nice
explanations contained within the standard :-) I'm not sure that my
interpretation of the standard is correct.  I would appreciate any
help that people fluent in LOTOS could provide me. The questions are
rather detailed and probably not of general interest, so e-mail
responses may be best to save on net traffic.

Given a LOTOS specification L, the semantics of L is defined by first
applying a 'flattening function' #.#, and then defining the transition
system in terms of the flattened specification #L#. However, the
function #.# is a partial function; LOTOS specifications which are not
in the domain of #.# do not fulfil the static semantic requirements.
Now the way I understand this, there exist LOTOS specifications which
are syntactically correct, but which have no semantics. This leads to
the following questions:
  -Is my understanding correct?
  -If yes, what are the class of syntactically correct LOTOS
   specifications which have no semantics?
  -Can it be statically determined whether a specification
   satisfies the static semantic requirements? (I sure hope so :-)

My second set of questions deals with the issue of unguarded
recursion. I have been warned by LOTOS experts to avoid the use of
unguarded recursion. However, one of the things which I have done as
part of my research is define a transformation phi, which transforms
one LOTOS spec into another. Given specification L, the transformed
spec phi(L) may contain unguarded recursion. This isn't really a
problem for me, provided that my interpretation of what unguarded
recursion means is correct.

For a specification L, the event a is accepted by L if there exists a
behaviour expression L' such that there exists a finite length
derivation according to the semantics of LOTOS which shows that L-a->L'.
Assume you have the following (pseudo-)LOTOS specification:

   P[a]
   where
    P[a] := a;P[a] ||| P[a]

The following derivation "proves" that P[a] -a-> (P[a]|||P[a]):

  a;P[a] -a-> P[a]                     -axiom b

  (a;P[a]|||P[a]) -a-> (P[a]|||P[a])   -inference rule g

  P[a] -a-> (P[a]|||P[a])              -inference rule k
                                         (process instantiation)

Further derivations can prove the following:

  if P[a] := a;P[a] || P[a]
  then P[a] deadlocks

  if P[a] := a;P[a] [] P[a]
  then P[a] -a-> P[a]

  if P[a] := exit ||| P[a]
  then P[a] deadlocks

Do I understand unguarded recursion? Are all the above statements
correct? Comments? Suggestions?

Thanks for any help that may be forthcoming.

================================================================
Mark Vigder

vigder@sce.carleton.ca

Dept. of Systems and Computer Engineering
Carleton University
Ottawa, Canada