Agent Skills: Temporal Logic Translator

Translate between temporal logic formalisms and generate property specifications

formal-verificationID: a5c-ai/babysitter/temporal-logic-translator

Install this agent skill to your local

pnpm dlx add-skill https://github.com/a5c-ai/babysitter/tree/HEAD/library/specializations/domains/science/computer-science/skills/temporal-logic-translator

Skill Files

Browse the full folder contents for temporal-logic-translator.

Download Skill

Loading file tree…

library/specializations/domains/science/computer-science/skills/temporal-logic-translator/SKILL.md

Skill Metadata

Name
temporal-logic-translator
Description
Translate between temporal logic formalisms and generate property specifications

Temporal Logic Translator

Purpose

Provides expert guidance on temporal logic specification and translation between formalisms.

Capabilities

  • LTL to Buchi automata
  • CTL to CTL* comparison
  • Natural language to temporal logic
  • Property pattern templates
  • Formula equivalence checking
  • Negation normal form conversion

Usage Guidelines

  1. Property Identification: Identify desired system properties
  2. Formalization: Express in appropriate temporal logic
  3. Translation: Convert between formalisms if needed
  4. Pattern Matching: Use property pattern templates
  5. Verification: Check formula equivalence

Tools/Libraries

  • Spot
  • GOAL
  • LTL2BA
  • NuSMV