CertiControl

Certificate-based analysis for continuous-time LTI systems, exposing the evidence behind controllability, observability, stability, LQR, and Kalman decomposition.

Comment

Inspiration

Classical control software is very good at computing answers, but many workflows stop at the answer itself: a system is reported as controllable, observable, stable, or not.

For learning, debugging, and small-scale engineering analysis, that is often not enough. We wanted to see the evidence behind the conclusion:

  • Which rank test produced the result?
  • Does the PBH criterion agree?
  • If controllability or observability fails, which mode causes the failure?
  • How small is the numerical residual?
  • Is the result sensitive to floating-point tolerance?
  • Can an exact symbolic calculation independently confirm it?

CertiControl grew from that idea: turn classical linear-control analysis into inspectable computational certificates rather than black-box Boolean outputs.

What it does

CertiControl analyzes continuous-time finite-dimensional LTI systems

[ \dot{x}=Ax+Bu,\qquad y=Cx+Du. ]

It currently provides certificate-based analysis for:

  • Controllability — controllability matrix, exact and numerical rank, PBH criterion, singular values, tolerance diagnostics, and explicit uncontrollable-mode witnesses.
  • Observability — observability matrix, PBH checks, unobservable-mode witnesses, duality checks, and exact/numerical diagnostics.
  • Stability and Lyapunov analysis — spectral abscissa, Hurwitz classification, exact rational and numerical Lyapunov certificates, positive-definiteness checks, and equation residuals.
  • LQR / CARE synthesis — Q/R validation, stabilizability and detectability checks, CARE solution, feedback gain, closed-loop stability, CARE residuals, and an independent closed-loop Riccati/Lyapunov identity check.
  • Kalman structural decomposition — reachable and unobservable subspaces, their intersection, all four controllable/observable structural dimensions, similarity transformation, structural-zero verification, and conditioning diagnostics.

The Streamlit interface lets users load curated examples or enter their own matrices, inspect the evidence behind each result, and export the complete analysis as Markdown or JSON.

How we built it

The project is written in Python.

The numerical path uses NumPy and SciPy, while SymPy provides exact rational algebra where appropriate. The interface is built with Streamlit, and Plotly is used for pole visualizations.

The architecture deliberately separates the mathematical core from the UI:

  1. matrix input is parsed and validated;
  2. each control-theory module produces a structured certificate;
  3. analyze_system() aggregates those certificates into a unified result;
  4. the reporting layer converts the result into Markdown or JSON;
  5. Streamlit only presents the existing certificate data and never reimplements the mathematics.

A major design goal was to combine exact and numerical computation without pretending they have the same strength. Exact algebraic conclusions are preserved when available, while numerical paths expose singular values, residuals, conditioning, and the tolerance actually used.

The repository currently contains 180 automated tests, with CI running on Python 3.10 and 3.13.

Challenges we ran into

The main challenge was not implementing individual textbook formulas, but making the different criteria agree in a useful and honest way.

Near rank-deficient or nearly unstable systems are inherently tolerance-sensitive. Instead of forcing every case into PASS or FAIL, CertiControl supports INCONCLUSIVE states and records the numerical evidence responsible for the ambiguity.

Another challenge was structural decomposition. A Kalman decomposition should not merely produce a change-of-basis matrix; the transformed system must satisfy the theoretically required zero-block structure. We therefore added explicit residual and structural checks, exact rational fixtures, duality tests, and similarity-invariance tests.

LQR required similar care. A small CARE residual alone is not sufficient evidence of a valid stabilizing solution, so the certificate also checks stabilizability, detectability, gain consistency, closed-loop Hurwitz stability, and the closed-loop Riccati/Lyapunov identity independently.

Accomplishments that we're proud of

The most important result is that CertiControl does not hide the reasoning behind its outputs.

For example, an uncontrollable system can return the offending eigenvalue and a left-eigenvector witness satisfying

[ q^\top A=\lambda q^\top,\qquad q^\top B=0, ]

together with its residual.

For Lyapunov analysis, exact rational inputs can produce an exact matrix (P) with a zero equation residual.

For LQR, the app shows the open-loop and closed-loop poles while independently verifying the CARE solution.

For the full Kalman decomposition, one curated four-state example contains exactly one state in each class:

[ (d_{co},d_{cu},d_{uo},d_{uu})=(1,1,1,1). ]

All of these results are available through both the Python API and the interactive interface.

What we learned

The project reinforced an important distinction between computing a result and providing evidence for a result.

Classical control theory already contains many equivalent criteria, invariance properties, residual identities, and structural witnesses. Treating those relationships as cross-checks makes software much easier to inspect and debug.

We also learned that exact symbolic and floating-point numerical computation work best as complementary tools rather than replacements for one another.

What's next

CertiControl is intentionally limited to small and medium-size continuous-time LTI systems for now.

Natural future extensions include:

  • discrete-time systems;
  • minimal realizations;
  • pole placement and observer design;
  • Kalman filtering and LQG;
  • model reduction;
  • deeper formal-verification connections.

For this release, however, the focus is deliberately narrow: make the existing classical analysis transparent, inspectable, and reproducible.

Built With

Share this project:

Updates

Submission history