[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php

Bibliographic Item (1.0)

Lamport95a

  1. Leslie Lamport
  2. TLA in Pictures
  3. IEEE Trans SE VSE-21n9(Sep 1995)pp768-775
  4. =THEORY TLA Formal Graphics temporal logic of actions
      Claims: first use of diagrams to provide complementary multiple formal views. an aid to presenttion and proof.

      Like FSA(states=>predicates, transactions => actions) out(n):edges out of n, d(e) :nodes=destination of edge e, P(n) :=predicate on node n, P'(n) :=primed predicate... disjoint_predicate:=for all nodes n1,n2(not(P(n1) and P(n2)).

      A(n) :=for some e:out(n)(action(n) and P'(d(e))) two possible formula for meaning of transitions:

    1. Δ:=for all nodes n, always(if P(n) then A(n) ) or
    2. Δ_bar:=always(some nodes n(P(n) and A(n))).
    3. (above)|-if Δ then Δ_bar
    4. (above)|-if disjoint_predicates then (Δ iff Δ_bar)


Search for bibliographic items containing a matching string.


(Search uses POSIX regular expressions and ignores case)

Search for a specific bibliographic item by name.



To see the complete bibliography (1Mb+) select:[Bibliography]