Skip to content

v0.1.0 - Initial Release

Choose a tag to compare

View all tags
@rizumita rizumita released this 12 May 23:54
· 67 commits to main since this release
v0.1.0
20eff4d
This commit was signed with the committer’s verified signature. The key has expired.
rizumita Ryoichi Izumita
GPG key ID: 5DB31762F998C905
Expired
Verified
Learn about vigilant mode.

This is the initial public release of TemporalKit, a Swift library for expressing, evaluating, and model-checking Linear Temporal Logic (LTL) formulas.

Key Features:

  • Type-safe LTL Representation: Define LTL formulas using a Swift-native enum structure.
  • Expressive DSL: Construct formulas intuitively with an idiomatic Swift DSL (.globally, .eventually, .until, etc.).
  • Trace Evaluation: Check if an LTL formula holds for a given execution trace (sequence of states) using LTLFormulaTraceEvaluator.
  • LTL Model Checking: Verify LTL formulas against finite-state system models (KripkeStructure) using advanced algorithms:
    • Translation of LTL formulas to Generalized Büchi Automata (GBA).
    • Optimized GBA acceptance condition generation, including special handling for the Release operator.
    • Efficient Büchi Automaton emptiness checking using an enhanced Nested DFS algorithm.
  • Formula Normalization: Automatic simplification of formulas (e.g., double negation elimination, constant propagation).
  • Extensible Design: Core protocols (TemporalProposition, EvaluationContext, KripkeStructure) allow for customization and extension.
  • Comprehensive Testing: Includes unit tests, integration tests, edge case handling tests, performance benchmarks, and random tests for robustness.
  • Demo Application: See Sources/TemporalKitDemo for practical usage examples.

This release provides a solid foundation for working with LTL in Swift projects, particularly for formal verification and analysis tasks.

Assets 2
Loading