Skip to content
KortexyaKortexyaReasoning Layer SDK

Interface: TemporalModelCheckRequest

@kortexya/reasoninglayer

@kortexya/reasoninglayer / TemporalModelCheckRequest

Interface: TemporalModelCheckRequest

Section titled “Interface: TemporalModelCheckRequest”

Defined in: src/types/temporal.ts:161

Request to check a CTL formula against an explicit finite Kripke structure.

Remarks

Section titled “Remarks”

Stateless and tenant-free: the model is supplied in full and checked in-process. initialStates must be a subset of the declared state IDs, and both endpoints of every transition must be declared in states.

Example

Section titled “Example”
const request: TemporalModelCheckRequest = {
  states: [
    { id: 0, labels: ['red'] },
    { id: 1, labels: ['green'] },
  ],
  transitions: [{ from: 0, to: 1 }, { from: 1, to: 0 }],
  initialStates: [0],
  formula: { op: 'ef', inner: { op: 'atom', name: 'green' } },
};

Properties

Section titled “Properties”

formula

Section titled “formula”

formula: CtlFormula

Defined in: src/types/temporal.ts:172

The CTL formula tree to check.

initialStates

Section titled “initialStates”

initialStates: number[]

Defined in: src/types/temporal.ts:169

States from which checking begins. Must be non-empty.

states

Section titled “states”

states: KripkeState[]

Defined in: src/types/temporal.ts:163

States in the Kripke model. Must be non-empty with unique IDs.

transitions?

Section titled “transitions?”

optional transitions?: KripkeTransition[]

Defined in: src/types/temporal.ts:166

Transition relation. Both endpoints must appear in states.