Class CTL<S,P>

java.lang.Object
org.episteme.core.mathematics.logic.temporal.CTL<S,P>
public class CTL<S,P> extends Object
Computation Tree Logic (CTL).

CTL is a branching-time temporal logic used for model checking. It extends propositional logic with temporal operators: - AG φ: φ holds on All paths Globally - EG φ: φ holds on some path Globally - AF φ: φ holds on All paths Finally - EF φ: φ holds on some path Finally - A[φ U ψ]: φ Until ψ on All paths - E[φ U ψ]: φ Until ψ on some path

Since:
1.0
Author:
Silvere Martin-Michiellot, Gemini AI (Google DeepMind)

  • Constructor Details

    • CTL

      public CTL()
      Creates an empty CTL model.

  • Method Details

    • addState

      public void addState(S state)
      Adds a state to the model.
      Parameters:
      state - the state to add

    • addTransition

      public void addTransition(S from, S to)
      Adds a transition between states.
      Parameters:
      from - the source state
      to - the target state

    • label

      public void label(S state, P proposition)
      Labels a state with an atomic proposition.
      Parameters:
      state - the state
      proposition - the proposition

    • holds

      public boolean holds(S state, P proposition)
      Checks if a proposition holds in a state.
      Parameters:
      state - the state
      proposition - the proposition
      Returns:
      true if the proposition holds

    • AG

      public Set<S> AG(Predicate<S> phi)
      AG φ: φ holds on All paths Globally.
      Parameters:
      phi - the predicate
      Returns:
      the set of states where AG φ holds

    • EG

      public Set<S> EG(Predicate<S> phi)
      EG φ: φ holds on some path Globally.
      Parameters:
      phi - the predicate
      Returns:
      the set of states where EG φ holds

    • EF

      public Set<S> EF(Predicate<S> phi)
      EF φ: φ holds on some path Finally.
      Parameters:
      phi - the predicate
      Returns:
      the set of states where EF φ holds

    • AF

      public Set<S> AF(Predicate<S> phi)
      AF φ: φ holds on All paths Finally.
      Parameters:
      phi - the predicate
      Returns:
      the set of states where AF φ holds

    • EU

      public Set<S> EU(Predicate<S> phi, Predicate<S> psi)
      E[φ U ψ]: φ Until ψ on some path.
      Parameters:
      phi - the first predicate
      psi - the second predicate
      Returns:
      the set of states where E[φ U ψ] holds

    • getStates

      public Set<S> getStates()
      Returns all states in the model.
      Returns:
      the set of all states

    • toString

      public String toString()
      Overrides:
      toString in class Object