AgentSkillsCN

temporal-logic-translator

在时序逻辑各形式之间进行转换，并生成属性规范

SKILL.md
--- frontmatter
name: temporal-logic-translator
description: Translate between temporal logic formalisms and generate property specifications
allowed-tools:
  - Bash
  - Read
  - Write
  - Edit
  - Glob
  - Grep
metadata:
  specialization: computer-science
  domain: science
  category: formal-verification
  phase: 6

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