Class LTL

java.lang.Object

org.episteme.core.mathematics.logic.temporal.LTL

public class LTL
extends Object

Linear Temporal Logic (LTL) implementation.

Provides semantics for evaluating LTL formulas over a linear sequence of states.

Since:

1.0

Author:

Silvere Martin-Michiellot, Gemini AI (Google DeepMind)

Constructor Summary

Constructors

Constructor	Description
LTL()

Method Summary

Modifier and Type	Method	Description
boolean	evaluateImplication(String formula, boolean p, boolean q)	Evaluates a simple implication formula "P -> Q".
boolean	next(List<Boolean> trace, int currentIndex, boolean property)	Evaluates if a property holds in the next state.
boolean	validate(String formula, List<String> allowedAxioms)	Validates if a formula is an allowed axiom.

Methods inherited from class Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

LTL

public LTL()

Method Details

next

public boolean next(List<Boolean> trace,
 int currentIndex,
 boolean property)

Evaluates if a property holds in the next state.

Parameters:

trace - sequence of states (valuations)

currentIndex - current time step

property - the property to check

Returns:

true if property holds in the next state

validate

public boolean validate(String formula,
 List<String> allowedAxioms)

Validates if a formula is an allowed axiom.

Parameters:

formula - the formula to check

allowedAxioms - list of allowed axioms

Returns:

true if allowed

evaluateImplication

public boolean evaluateImplication(String formula,
 boolean p,
 boolean q)

Evaluates a simple implication formula "P -> Q".

Parameters:

formula - the formula string

p - truth value of antecedent P

q - truth value of consequent Q

Returns:

truth value of P -> Q