{"uid":"cap_Oor10_l5LBZvWu-aRY-7Z","slug":"finite-kripke-ctl-branching-time-satisfaction-sets-verifier-225577d8","name":"Finite Kripke CTL Branching-Time Satisfaction Sets Verifier","description":"Verify every CTL state satisfaction set of a supplied total finite branching-time model.","url":"https://detect.halowerk.com/v1/F-REST-B20/finite-total-kripke-ctl-branching-time-satisfaction-sets?utm_source=zero.xyz","method":"POST","headers":{},"bodySchema":{"type":"object","properties":{"artifact":{"type":"object","required":["ctl"],"properties":{"ctl":{"type":"object","required":["data","claim"],"properties":{"data":{"type":"object","required":["n","edges","labels","formulas"],"properties":{"n":{"type":"integer","maximum":8,"minimum":1},"edges":{"type":"array","items":{"type":"array","items":{"type":"integer","maximum":255,"minimum":0},"maxItems":2,"minItems":2},"maxItems":64,"minItems":0},"labels":{"type":"array","items":{"type":"array","items":{"type":"integer","maximum":255,"minimum":0},"maxItems":16,"minItems":0},"maxItems":8,"minItems":1},"formulas":{"type":"array","items":{"anyOf":[{"type":"object","required":["op","proposition"],"properties":{"op":{"const":"atom"},"proposition":{"type":"integer","maximum":255,"minimum":0}},"additionalProperties":false},{"type":"object","required":["op","body"],"properties":{"op":{"enum":["not","EX","AX","EG","AG","EF","AF"]},"body":{"type":"integer","maximum":255,"minimum":0}},"additionalProperties":false},{"type":"object","required":["op","left","right"],"properties":{"op":{"enum":["and","or","EU","AU"]},"left":{"type":"integer","maximum":255,"minimum":0},"right":{"type":"integer","maximum":255,"minimum":0}},"additionalProperties":false}]},"maxItems":40,"minItems":1}},"additionalProperties":false},"claim":{}},"additionalProperties":false}},"additionalProperties":false}}},"responseSchema":null,"example":null,"exampleRequest":null,"tags":["x402"],"displayCostAmount":"0.003","displayCostAsset":"USDC","priceDynamic":false,"priceHint":null,"priceStatus":"priced","priceSource":"probe","requiresHandshake":false,"reviewCount":0,"rating":{"score":"0.00","successRate":"0.00","reviews":0,"stars":null,"state":"unrated"},"availabilityStatus":"unknown","priceObserved":null,"sessionDeposit":null,"pricing":{"kind":"static","summary":"$0.003/call","primary":{"kind":"static","protocol":"x402","network":"base","amountUsd":"0.003","per":"call","confidence":"exact"},"accepted":[{"kind":"static","protocol":"x402","network":"base","amountUsd":"0.003","per":"call","confidence":"exact"}]},"paymentMethods":[{"uid":"pm_8TAs4I6mFgUd08IP0IZYw","protocol":"x402","methodType":"crypto","chain":"base","mode":"charge","costAmount":"0.003","costPer":"request","priority":0,"asset":"0x833589fCD6eDb6E08f4c7C32D4f71b54bdA02913","unit":"request","depositMicros":null,"planRef":null}],"brandName":null,"brandSlug":null,"brandBaseUrl":null,"brandDocsUrl":null,"whatItDoes":"Computes the satisfaction set of every CTL formula over a supplied finite total Kripke structure, verifying all branching-time temporal logic claims.","exampleAgentPrompt":"I have a finite Kripke structure with 3 states, edges [[0,1],[1,2],[2,1]], per-state label sets [[0],[1],[0,1]], and two CTL formulas — atom(0) and EG(atom(1)) — can you compute the satisfaction set for each formula over this model?","exampleUseCases":[{"title":"CTL reachability verification for protocol model","prompt":"I'm modeling a communication protocol as a Kripke structure with 4 states, edges [[0,1],[1,2],[2,3],[3,1]], labels [[0],[1],[2],[1,2]], and I want to verify which states satisfy the EF formula for proposition 2 and the AG formula for proposition 0 — please give me the satisfaction sets for both."},{"title":"Safety property check on a small state machine","prompt":"I have a 5-state system modeled as a Kripke structure with edges [[0,1],[0,2],[1,3],[2,3],[3,4],[4,3]], labels [[0,1],[1],[2],[0,2],[1,2]], and formulas AG(atom(0)) and AF(atom(2)) — which states satisfy each formula?"},{"title":"Branching-time logic homework verification","prompt":"Can you verify my CTL model checking work? I have a 2-state Kripke structure with edges [[0,1],[1,0]], labels [[0],[1]], and three formulas: atom(0), EX(atom(1)), and AX(atom(0)) — tell me the exact satisfaction set for each."}],"resultDescription":"Returns the satisfaction set for every CTL formula provided — i.e., the set of state indices (from 0 to n-1) that satisfy each formula in the given finite total Kripke structure. Results allow verification of branching-time temporal logic claims against the model.","failureModes":["Invalid graph: edges reference state indices >= n","Non-total structure: some state has no outgoing edge (violates totality constraint)","Formula references undefined sub-formula index (out of bounds)","n exceeds maximum of 8 or is below minimum of 1","Formula count exceeds 40 or edges exceed 64","Malformed formula operator not in allowed enum","Cycle or formula index self-reference causing invalid evaluation order"],"whenToPreferThis":"Use this endpoint when you need to formally verify CTL (Computation Tree Logic) satisfaction sets over a small finite total Kripke structure (up to 8 states, 64 edges, 40 formulas). It is ideal for model checking tasks involving branching-time temporal operators (EX, AX, EG, AG, EF, AF, EU, AU) on finite automata, protocol verification, or academic CTL exercises. Prefer this over custom implementations when you need a reliable, hosted model checker for bounded-size models without writing your own fixpoint algorithms.","instructions":null,"reviewSummary":null,"reviewSummaryHighlights":null,"reviewSummaryConcerns":null,"reviewSummaryGeneratedAt":null,"activationCount":0,"lastUsedAt":null,"lastSuccessfullyRanAt":null,"lastHealthCheckAt":"2026-11-01T06:50:58.951Z","isFirstParty":false,"canonicalSlug":"finite-kripke-ctl-branching-time-satisfaction-sets-verifier-225577d8"}