diff --git a/.gitignore b/.gitignore index 2ea282f..426f467 100644 --- a/.gitignore +++ b/.gitignore @@ -36,6 +36,9 @@ Thumbs.db *.swo .vscode/ .idea/ + +# Claude Code +CLAUDE.md *.sty .DS_Store *.aux diff --git a/CLAUDE.md b/CLAUDE.md deleted file mode 100644 index 5f4c440..0000000 --- a/CLAUDE.md +++ /dev/null @@ -1,133 +0,0 @@ -# CLAUDE.md - -This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository. - -## Project Overview - -This is a PhD thesis proposal for developing a methodology to build High-Assurance Hybrid Autonomous Control Systems (HAHACS) for critical infrastructure. The proposal is titled "From Cold Start to Critical: Formal Synthesis of Autonomous Hybrid Controllers." - -**Intellectual Merit**: The contribution is architectural unification rather than algorithmic novelty. The methodology provides a systematic decomposition mapping verification techniques to control mode types, composing existing formal methods into a complete framework where none existed. - -**Key Insight**: The methodology formalizes EXISTING discrete abstractions from operating procedures (especially nuclear) rather than imposing arbitrary ones. Operating procedures already define go/no-go conditions as discrete predicates - this work provides the formalization and verification framework. - -## Document Structure - -The proposal uses a modular LaTeX structure with numbered section directories: -- `main.tex` - Root document that inputs all sections -- `1-goals-and-outcomes/` - Research statement and goals -- `2-state-of-the-art/` - Literature review -- `3-research-approach/` - Core methodology (CURRENTLY ACTIVE WORK) -- `4-metrics-of-success/` - Success criteria -- `5-risks-and-contingencies/` - Risk analysis -- `6-broader-impacts/` - Broader impacts -- `8-schedule/` - Timeline - -Each section directory contains: -- `v1.tex` (or `v2.tex` for actively revised sections) - Main content -- `outline.md` (optional) - Planning notes and structure - -**IMPORTANT**: Section 3 (research-approach) is currently being revised. `main.tex` inputs `v2.tex` for this section, which contains extensive inline comments and questions prefixed with `%` and `% Q:`. - -## Building the Document - -```bash -# Full build with bibliography -pdflatex main.tex -bibtex main -pdflatex main.tex -pdflatex main.tex - -# Quick build (no bibliography updates) -pdflatex main.tex - -# Use latexmk for automated builds -latexmk -pdf main.tex - -# Clean auxiliary files -latexmk -c -``` - -The output is `main.pdf`. - -## Key Technical Concepts - -### Mathematical Notation -- **Continuous state space**: X ⊆ ℝⁿ -- **Discrete modes**: Q = {q₁, q₂, ...} -- **Per-mode continuous regions**: X_entry,i, X_exit,i, X_safe,i -- **Discrete predicates**: pᵢ: X → {true, false} (Boolean functions over continuous state) - -### Three Control Mode Types -Each mode type has distinct control objectives and verification methods: - -1. **Transitory modes**: Transition between discrete states - - Objective: reach(X_entry) → reach(X_exit) while maintaining x(t) ∈ X_safe - - Verification: Reachability analysis - - Formal: Reach(X_entry, f(x,u), T) ⊆ X_exit ∪ X_safe - -2. **Stabilizing modes**: Maintain steady state - - Objective: remain(X_target) where X_target ⊂ X_safe - - Verification: Barrier certificates - - Formal: ∇B(x)·f(x,u) ≤ 0 on boundary ∂X_safe - -3. **Expulsory modes**: Safe shutdown under failures - - Objective: reach(X_current) → reach(X_safe_shutdown) under parametric uncertainty - - Verification: Parametric robust reachability - - Formal: Reach(X_current, f(x,u,θ), T) ⊆ X_safe_shutdown for all θ ∈ Θ_failure - -### Scope Boundaries -- **Verify** continuous controllers, not **synthesize** them (analogous to model checking) -- Assume controllers can be designed using standard control theory -- Contribution is verification that candidate controllers compose correctly with discrete layer - -## Active Development Context - -### Current Focus (as of 2026-01-26) -Editing the research approach section (`3-research-approach/v2.tex`) with a Wednesday (2026-01-28) draft deadline. - -### Open Technical Questions -Questions are embedded in `v2.tex` comments. Key unresolved issues: - -**Easier to address:** -- Hysteresis and sensor noise handling (standard control theory) -- Mealy machine formalization (presentation issue) -- Failure detection scope boundaries (precision in claims) - -**More challenging:** -- Timing constraint verification (timed automata integration) -- Parametric uncertainty bounds methodology -- Numerical precision in discrete abstraction (task 36 in taskwarrior) -- Controller design gap (scope vulnerability) - -### Taskwarrior Integration -The user tracks tasks in taskwarrior. The Thesis project has ~45 tasks including: -- 9 writing tasks for research approach sections (due 2026-01-28) -- Multiple reading tasks on hybrid systems, reachability, formal methods -- Outstanding question (task 36): "How do we handle numerical barriers when creating discrete automata?" - -Use `task list project:Thesis` to see current tasks. - -## Bibliography - -References are in `references.bib` using IEEE transaction format. The bibliography includes: -- Hybrid systems theory and verification -- Formal methods (reactive synthesis, temporal logic) -- Control theory (reachability, barrier certificates) -- Nuclear regulatory documents (NUREG, 10 CFR) -- Industrial control systems - -## Custom LaTeX Class - -`dane_proposal_format.cls` provides: -- NSF-compliant formatting (Times New Roman, 1" margins) -- Custom `\task{title}{description}` command for numbered tasks -- TikZ libraries for diagrams -- Table and figure formatting -- Default metadata (title, author, advisor) - -## Writing Style Notes - -- Inline comments in `.tex` files starting with `%` are working notes -- Comments with `% Q:` indicate open questions requiring research/decisions -- Sections marked with `\iffalse ... \fi` are draft text, not compiled -- Text after `\iffalse` blocks are outlines/notes for future writing