Semantics of LTS

From: Jean-S?bastien Bolduc (jseb_at_cs.mcgill.ca)
Date: 10/22/04

  • Next message: Michael J. Fromberger: "Re: Multiple errors recognition" 
    Date: 21 Oct 2004 15:04:13 -0700

    I've seen Labeled Transition Systems (LTS) used to describe the
    semantics of various formalisms. However, I couldn't find a precise
    description of LTS's operational semantics. It first seemed pretty
    obvious, but I got confused when trying to derive LTS semantics from
    Milner's CCS...

    Consider the simple, "axiomatic" rule from CCS:
        a.P -(a)-> P
    The same behaviour is obtained by the LTS with a single transition
    (with label 'a') going from state s_0 to s_1, which correspond
    respectively to processes a.P and P. Simple enough. When in state s_0,
    the transition is always enabled.

    In CCS, there is a distinction between the set of names and co-names.
    By extension to LTS, I understand the first set as equivalent to the
    set of possible inputs to the LTS, and the set of co-names as
    equivalent to the set of possible outputs. Perhaps this is where I'm
    mistaken? So in the simple rule above I can conceive that the
    transition is always enabled if the label 'a' is an "output"; if 'a'
    is an "input" however, it seems to me there should be an extra
    condition for the transition to be enabled.

    Basically, the transition should be enabled only if the LTS is
    "receiving" the input... For such an LTS that is not running coupled
    with a generator process, the transition would never be enabled.

    Anybody could tell me what am I missing?

    Thank you

  • Next message: Michael J. Fromberger: "Re: Multiple errors recognition"

    Relevant Pages

    • Re: Semantics of LTS
      ... > I've seen Labeled Transition Systems (LTS) used to describe the ... > description of LTS's operational semantics. ... Before CCS advocates kill me because of this opinion, ... > condition for the transition to be enabled. ...
      (comp.theory)
    • Re: Semantics of LTS
      ... > description of LTS's operational semantics. ... but I got confused when trying to derive LTS semantics from ... > the transition is always enabled. ... > In CCS, there is a distinction between the set of names and co-names. ...
      (comp.theory)
    • Re: Semantics of LTS
      ... So the semantics of LTS could be described informally as: ... execute co-a and become a.P | Q ... An LTS is "more" than a finite automaton in that usually the semantics ...
      (comp.theory)