Defining Logic Formulas

This example demonstrates how to define logic formulas using iglsynth.logic module. Presently, IGLSynth defines three classes of logic formulas; namely atomic propositions AP, propositional logic PL and linear temporal logic LTL.

Atomic Propositions

The most common use of logic formulas in IGLSynth is to define certain properties of a game on graph. Hence, we define atomic propositions to be Callable objects over states (or vertices) of a graph.

An AP can be defined by providing a name:

a = AP(formula='a')

However, it is desirable to evaluate an AP at a given state. This can be achieved by instantiating an AP in the following way:

# Define atomic proposition with evaluation function
@ap
def is_goal(st):
    return st == 10

# Define atomic proposition with evaluation function accepting extra arguments
@ap
def is_colliding(st, *args):
    obs = args[0]
    return st in obs

# Define atomic proposition with evaluation function accepting extra keyword arguments
@ap
def is_close(st, **kwargs):
    threshold = kwargs['threshold']
    return st - threshold < 10

Let us understand the three AP definitions given above. The first AP, is_goal, accepts a state st as an input parameter and returns whether st == 10 or not. It is imperative that an AP must return a bool.

In many cases, it is convenient to define a parameterized atomic proposition. In such cases, the extra parameters can be passed to the AP’s evaluation function as optional arguments args or optional keyword arguments kwargs.

Note

It is strongly recommended that AP’s function template to have *args, **kwargs as parameters.

Given an AP, it is possible to evaluate it at a given state:

res = is_goal(10)
res = is_goal(20)

res = is_colliding(10, [5, 10])
res = is_colliding(20, [5, 10])

res = is_close(5, threshold=10)
res = is_close(50, threshold=10)

---

Propositional Logic Formulas

Propositional Logic Formulas can be defined by instantiating PL class. Similar to AP, a propositional logic formula can be defined by passing a formula string containing only And(&), Or(|) and/or Negation(!) operators:

plf0 = PL("a & b")
plf1 = PL("a | b")
plf2 = PL("!a | b")

A PL formula is, generally, defined over an alphabet. An alphabet is a set of atomic propositions. To define a PL formula over alphabet, first define an alphabet:

@ap
def a(st, *args, **kwargs):
    return st == 10

@ap
def b(st, *args, **kwargs):
    return st in args[0]

sigma = Alphabet([a, b])

An important feature of alphabet is that it can be evaluated at a given state. For example,:

result = sigma.evaluate(10, [10, 20])

returns a dictionary with keys as AP’s in alphabet and values as the result of evaluating the AP at given state. In above case, result = {a: True, b: True}.

Note

Observe that evaluating an alphabet at a state is equivalent to computing the label of that state.

Now, we can define a PL formula over an alphabet.

plf = PL("a & b", alphabet=sigma)

PL formulas can also be evaluated at a given state.

# PL is callable class
res = plf(10, [10, 20])

# Explicitly call evaluate function
res = plf.evaluate(10, [10, 20])

When a PL formula is evaluated at a given state, the alphabet is evaluated at that state. Then, the APs in PL formula are substituted with the evaluated values to get back True or False.

Warning

Calling PL object like res = plf(10, [10, 20]) is currently failing. See Bug Report Issue #17.

---

Temporal Logic Formulas

(Linear) Temporal Logic formulas can be defined by instantiating LTL class. Similar to PL, LTL formulas can be defined with/without providing an alphabet.

# Alphabet not provided.
ltlf0 = LTL(formula="Gp1 & !(p1 & X(p0 xor p1))")

# Alphabet provided
ltlf = LTL("F(a & Fb)", alphabet=sigma)