Specification To Temporal Logic Generator Agent Skill
Translate natural-language requirements or structured specification documents into formal temporal logic properties (LTL, CTL, safety/liveness properties). Use when users need to formalize requirements for model checking, formal verification, or property specification. Handles embedded/real-time systems, hardware verification, concurrent systems, and reactive systems. Resolves ambiguities, asks clarifying questions when needed, and outputs machine-checkable formulas with explanations. Supports multiple output formats (SPIN, NuSMV, Uppaal, TLA+, Maude).
Install
one command, takes just this skill from the repositorynpx skills add https://github.com/ArabelaTso/Skills-4-SE --skill specification-to-temporal-logic-generatorThe instruction itself
16 sections, as written by the authorSpecification-to-Temporal-Logic Generator
Translate natural-language requirements into formal temporal logic properties for model checking and formal verification.
Workflow
1. Parse Input Requirements
Extract requirements from natural language text, structured documents, or semi-formal notations.
Identify key elements:
- Events/Actions: What happens (e.g., "request", "response", "button_press")
- States/Conditions: System states (e.g., "authenticated", "locked", "idle")
- Temporal relationships: When things happen (e.g., "always", "eventually", "before")
- Quantification: Scope (e.g., "every", "some", "at least once")
2. Identify Property Type
Classify requirements:
Safety (something bad never happens): Keywords "never", "always not", "must not" → G(!bad_event)
Liveness (something good eventually happens): Keywords "eventually", "will", "guaranteed" → F(good_event)
Response (if X then eventually Y): Keywords "whenever", "if...then", "leads to" → G(X -> F Y)
Precedence (X before Y): Keywords "before", "precedes", "only after" → (!Y) U X
Fairness (repeated opportunities): Keywords "infinitely often", "repeatedly" → G F X
3. Handle Ambiguities
When requirements are ambiguous:
Check common ambiguities: temporal scope, quantification, ordering, duration
Ask clarifying questions:
"The system responds to requests" could mean:
1. Every request eventually gets a response: G(request -> F response)
2. Some requests get responses: EF(request && response)
Which interpretation matches your intent?
State assumptions explicitly:
Formula: G(request -> F response)
Assumptions:
- "Every request" means all requests (universal quantification)
- "Responds" means eventually, with no time bound
See ambiguity_resolution.md for detailed patterns.
4. Select Appropriate Logic
Use LTL for single execution paths, "infinitely often" (G F), "eventually forever" (F G)
Use CTL for branching time, "on all paths" (A) vs "on some path" (E), reachability
5. Generate Formulas
Match to pattern: See ltl_patterns.md and ctl_patterns.md
Instantiate pattern:
Pattern: G(p -> F q)
Requirement: "Every request gets a response"
Formula: G(request -> F response)
Validate syntax:
python scripts/validate_formula.py "G(request -> F response)" LTL
Add explanations: Plain English, formal semantics, assumptions, counterexamples
6. Convert to Tool-Specific Syntax
Generate formulas for target tools using conversion script:
python scripts/convert_format.py "G(request -> F response)" LTL SPIN
See tool_syntax.md for complete syntax reference.
Output Format
For each requirement:
Requirement: [Original requirement]
Formula (LTL): [LTL formula]
Formula (CTL): [CTL formula, if applicable]
Property Type: [Safety/Liveness/Response/Precedence/Fairness]
Explanation:
- Plain English: [What it means]
- Formal Semantics: [Technical interpretation]
- Assumptions: [List of assumptions]
- Violation Example: [What would violate this]
Tool-Specific Syntax:
- SPIN: [Promela syntax]
- NuSMV: [NuSMV syntax]
- Uppaal: [Uppaal syntax]
Validation: [Result from validate_formula.py]
Examples
Safety Property
Requirement: "The system never enters a deadlock state"
Output:
Formula (LTL): G(!deadlock)
Formula (CTL): AG(!deadlock)
Property Type: Safety (Invariant)
Explanation:
- Plain English: The system never reaches a deadlock state
- Formal Semantics: At all time points, deadlock does not hold
- Assumptions: "deadlock" is a well-defined state predicate
- Violation: System reaches a state where no process can progress
Tool-Specific Syntax:
- SPIN: [] (!deadlock)
- NuSMV: SPEC AG(!deadlock)
- Uppaal: A[] not deadlock
Response Property
Requirement: "Whenever a button is pressed, the light turns on within 3 time units"
Output:
Formula (TCTL): G(button_press -> F[<=3] light_on)
Property Type: Bounded Response (Liveness)
Explanation:
- Plain English: Every button press is followed by light turning on within 3 time units
- Assumptions: Time is discrete, light can turn on multiple times
- Violation: Button pressed but light doesn't turn on within 3 time units
Tool-Specific Syntax:
- Uppaal: A[] (button_press imply A<> light_on[<=3])
Precedence Property
Requirement: "Users must authenticate before accessing the system"
Output:
Formula (LTL): (!access) U authenticated
Formula (CTL): A[(!access) U authenticated]
Property Type: Precedence (Safety)
Explanation:
- Plain English: No access occurs until authentication happens
- Assumptions: Authentication is one-time, access can occur multiple times after
- Violation: Access occurs before authentication
Tool-Specific Syntax:
- SPIN: ((!access) U authenticated)
- NuSMV: SPEC A[(!access) U authenticated]
Resources
scripts/
validate_formula.py- Validate temporal logic syntax (LTL, CTL, SPIN)convert_format.py- Convert between tool formats (SPIN, NuSMV, Uppaal, TLA+, Maude)
references/
ltl_patterns.md- LTL property patterns and templatesctl_patterns.md- CTL property patternsambiguity_resolution.md- Guidelines for handling ambiguous requirementstool_syntax.md- Syntax for different model checkers
Other skills for the same job
different authors, same section of the catalogue
Convert Markdown files to HTML similar to `marked.js`, `pandoc`, `gomarkdown/markdown`, or similar tools; or writing custom script to convert markdown to html and/or working on web template systems like `jekyll/jekyll`, `gohugoio/hugo`, or similar web templating systems that utilize markdown documents, converting them to html. Use when asked to "convert markdown to html", "transform md to html", "render markdown", "generate html from markdown", or when working with .md files and/or web a templating system that converts markdown to HTML output. Supports CLI and Node.js workflows with GFM, CommonMark, and standard Markdown flavors.
Write and maintain technical documentation. Trigger with "write docs for", "document this", "create a README", "write a runbook", "onboarding guide", or when the user needs help with any form of technical writing — API docs, architecture docs, or operational runbooks.
Translate visa application documents (images) to English and create a bilingual PDF with original and translation
Write, review, and edit documentation files with consistent structure, tone, and technical accuracy. Use when creating docs, reviewing markdown files, writing READMEs, updating `/docs` directories, or when user says "write documentation", "review this doc", "improve this README", "create a guide", or "edit markdown". Do NOT use for code comments, inline JSDoc, or API reference generation.
Real-time Constitution compliance checker for devflow documents. Blocks partial implementations and hardcoded secrets during file editing.
Write self-documenting code with minimal, evergreen comments that explain complex logic without describing recent changes or temporary fixes. Use this skill when writing code comments, documentation strings, explaining complex algorithms, clarifying business logic, or deciding whether code needs comments. Apply when working with any source code files where comments or documentation might be added, ensuring comments remain relevant, helpful, and focused on explaining why rather than what the code does, while preferring clear code structure and naming over excessive commenting.
Use when writing technical documentation that needs to be readable by both humans and AI models, converting existing docs to HADS format, validating a HADS document, or optimizing documentation for token-efficient AI consumption.
Draft a structured investment committee memo for PE deal approval. Synthesizes due diligence findings, financial analysis, and deal terms into a professional IC-ready document. Use when preparing for investment committee, writing up a deal, or creating a formal recommendation. Triggers on "write IC memo", "investment committee memo", "deal write-up", "prepare IC materials", or "recommendation memo".
How to use it
Take arabelatso/specification-to-temporal-logic-generator from the repository into ~/.claude/skills for personal
use, or into .claude/skills inside a project.
The agent identifies a skill by the name field in its header. Two skills with the
same name cannot sit side by side — one of them will be ignored.