You are here

ABSTEM

ABSTEM is a tool for computing temporal equilibrium models of arbitrary temporal theories. This tool represents the Temporal Equilibrium Models of an input temporal theory in terms of a Büchi automaton, which is built  using an automata-based aproach [CD11].   

  • Setting up :

ABSTEM has dependencies with both SPoT (≥ 1.0.2), a library to operate with ω-automata, and Graphviz, an open source graph visualization sofware. Once these dependencies are met, ABSTEM can be easily compiled using the make command:

  • cd path-to-abstem.
  • make && make install
  • Input Syntax:

ABSTEM reads an LTL theory from the standard input and computes its Temporal Equilibrium Models in terms of a Büchi automaton. In order to build the input theory, ABSTEM defines the following operators:  

  Constants Unary operators (prefix) Binary operators (infix)
Boolean
  • false: 0, false.
  • true: 1, true.
  • not: !, ~.
  • and: &, &&, /\.
  • or: |, ||, +, \/.
  • xor: xor, ^
  • implies: ->, -->, =>.
  • equivalent: <->, <-->, <=>.
LTL  
  • eventually: F, <>.
  • always: G, [].
  • next: X, ().
  • (strong) until: U.
  • (weak) release: R, V.
  • weak until: W.
  • strong release: M.

Use alphanumeric identifiers or double-quoted strings for atomic propositions, and parentheses for grouping. Identifiers cannot start with the letter of a prefix operator (F, G, or X): for instance GFa means G(F(a)). Use "GFa" if you really want to refer to GFa as a proposition. Conversely, infix letter operators are not assumed to be operators if they are part of an identifier: aUb is an atomic proposition, unlike a U b and (a)U(b).

  • Command-Line options:

    The computation of the TEM of an input theory is made by the computation of several intermediate ω-automata which can be also displayed by several command-line options. Being µ an input theory, h(µ'') the filtered automaton [CD11], and L(µ) the Büchi automaton which accepts the theory µ, every intermediate automaton can be displayed by the following command-line options:    

Automaton Option Output File
 L(µ)  --SForm ltl.png
L(µ'') --NonTot ntot.png
L(h(µ'')) --SFiltered filtered.png
comp(L(h(µ''))) --SComp comp.png
Final Automaton   models.png

In order to obtain a more readable output, the resulting automaton can be minimised using the command-line option -m.  

  • Examples:
    • a U b:
      • Command: abstem -t -m -l "a U b"

 

  • a R b:
    • Command: abstem -t -m -l "a R b"

 

  • [](!p => X p):
    • Command: abstem -m -t -l "[](!p=>Xp)"

   

  •  (!r->p)&&G(p->(Xp|Xs))&&G((s&!p)->Xp)&&(GFp->q):
    • Command:  abstem -m -t -l "'(!r->p)&&G(p->(Xp|Xs))&&G((s&!p)->Xp)&&(GFp->q)"

 

 

  • (!"u(2,f)"->"u(2,t)")&&(!"u(2,t)"->"u(2,f)")&&(!"u(1,f)"->"u(1,t)")&&(!"u(1,t)"->"u(1,f)")&&[](!!X"t(2)"->X"t(2)")&&[](!!X"t(1)"->X"t(1)")&&(!!"t(2)"->"t(2)")&&(!!"t(1)"->"t(1)")&&[](X"u(2,t)"->X"off")&&("u(2,t)"->"off")&&[](X"u(1,t)"->X"off")&&("u(1,t)"->"off")&&[](X"u(1,f)"&&X"u(2,f)"->X"on")&&("u(1,f)"&&"u(2,f)"->"on")&&[]("u(2,t)"&&!X"u(2,f)"->X"u(2,t)")&&[]("u(2,f)"&&!X"u(2,t)"->X"u(2,f)")&&[]("u(1,t)"&&!X"u(1,f)"->X"u(1,t)")&&[]("u(1,f)"&&!X"u(1,t)"->X"u(1,f)")&&[]("t(2)"&&"u(2,f)"->X"u(2,t)")&&[]("t(2)"&&"u(2,t)"->X"u(2,f)")&&[]("t(1)"&&"u(1,f)"->X"u(1,t)")&&[]("t(1)"&&"u(1,t)"->X"u(1,f)")&&[]((!"t(1)"&&!"t(2)")->false)&&[](("t(1)"&&"t(2)")->false)&&[](("on"&&"off")->false)&&[](("u(2,t)"&&"u(2,f)")->false)&&[](("u(2,f)"&&"u(2,t)")->false)&&[](("u(1,t)"&&"u(1,f)")->false)&&[](("u(1,f)"&&"u(1,t)")->false):
    • Command: abstem -m -t -f examples/ex4.abs

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

  • []<>p:
    • Command: abstem -t -m -l "echo '[]<>p"