scratch
§ Model Checking For Streaming Automata Ala CIRCT Handshake
created 2026-09-11
- Just treat the automata as having natural number, monotonic state which is the 'cursor' of where we are ponting in the stream.
- The transitions are then a function of the current state? And it should all be LIA?
- So, PDR style techniques (yay Nikolaj) should allow us to do stream verification on these?
- However, the issue is that FSM with two counters can simulate a TM.
- However! We have a monotonicity criterion, which restricts what can be done. So maybe something can be done here?
❦