Implement comprehensive LTL model checking feature

[Kuniwak]

This commit adds a complete Linear Temporal Logic (LTL) model checking capability to the CSP interpreter using the automata-theoretic approach.

Core Components Added:

• LTL formula AST with support for all standard temporal operators
• S-expression parser for LTL formulas
• Complete Büchi automaton construction using tableau method
• Product automaton construction for CSP processes and Büchi automata
• Emptiness checking with counterexample generation
• Automaton optimization (dead state removal, minimization)
• New CLI command: csp check

Key Features:

• Supports full LTL syntax: X, F, G, U, R operators
• Tableau-based Büchi automaton generation with closure computation
• Efficient state space exploration with optimizations
• Counterexample generation for property violations
• Integration with existing CSP state space generation

Technical Implementation:

• Uses standard automata-theoretic model checking algorithm
• Implements closure computation and elementary sets for tableau construction
• Proper handling of acceptance conditions for Until formulas
• State space optimizations: unreachable/dead state removal, equivalence merging
• Product automaton construction with synchronized transitions

Example Usage:
csp check examples/ParABC.sexp "(unwind P)" "(ltl (finally (atom A)))"

This enables verification of temporal properties like safety, liveness, and fairness constraints on CSP concurrent systems.

🤖 Generated with Claude Code