Cyber-Physica/Control systems and Game Semantics Formalization

[BasharHamade12]

Overview

This PR adds formalization of control systems theory and game semantics to CSLib.

What's included

Control Systems (CPS) - Discrete-time Linear Systems

• Basic.lean: Core definitions for discrete-time linear systems, state-space representation, and zero input
• AsymptoticStability.lean: Asymptotic stability analysis using spectral radius and Gelfand formula
• Cayley.lean: Cayley-Hamilton theorem applications for controllability
• Controllability.lean: Controllability and reachability analysis
• Reachability.lean: State reachability characterization

Game Semantics

• HMLGame.lean: Game semantics interpretation of Hennessy-Milner Logic (HML)## Overview
  This PR adds formalization of control systems theory and game semantics to CSLib.

What's included

Control Systems (CPS) - Discrete-time Linear Systems

• Basic.lean: Core definitions for discrete-time linear systems, state-space representation, and zero input
• AsymptoticStability.lean: Asymptotic stability analysis using spectral radius and Gelfand formula
• Cayley.lean: Cayley-Hamilton theorem applications for controllability
• Controllability.lean: Controllability and reachability analysis
• Reachability.lean: State reachability characterization

Game Semantics

• HMLGame.lean: Game semantics interpretation of Hennessy-Milner Logic (HML)

Key Theorems

• asymptotic_stability_discrete: If spectral radius < 1, zero-input response converges to zero
• cayley_hamilton_controllability': Higher powers of system matrix lie in span of first n powers
• Game-theoretic characterization of HML satisfaction
• full_finrank_equivalent_to_reachability: The Kalman Controllability Rank Condition —
  A system is reachable if and only if the controllability matrix has full rank (finrank equals dimension).
  -/

[ctchou]

First, please run lake exe mk_all --module, so that you can generate the correct formats for Cslib.lean and CslibTests.lean. Please also take a look at the existing files to see the correct format for imports and other module related things at the beginning of each code file.

This is a subject that is perhaps unfamiliar to most people with a standard computer science background. Perhaps you can provide some references? You can put it references.bib and refer to them in comments in your code.

[fmontesi]

I'm not an expert in CPS models but it is certainly relevant for CSLib. I wonder if this should be split into multiple PRs though, as it's quite big and it really introduces at least three concepts: CPS, games, and (a game semantics interpretation of) HML (and we don't even have 'normal' HML on LTS yet). I'm a bit overwhelmed. :-)

[BasharHamade12]

• I have adapted the changes you have suggested into my fork , basically CPS has been something I have been working on for a long time with my supervisor from my uni , so I had too much already accumulated . Would it be better if I maybe first do a PR with a subset of the things from there (for example, just 'Basic.lean' and 'AsymptoticStability.lean') and afterwards try to contribute the rest of the stuff?

• Regarding Game semantics and HML, it is a project I am working on right now and thought would be nice to have in Cslib as well, I will do as you suggested and have it as a separate PR .

• I will also work on having better linting and less warnings .

Does that sound like a solid approach ?