Verification of Parametric Counter Automata in a Dependently Typed Language
Christoph A. Herrmann, Edwin C. Brady, Kevin L Hammond · 2009
Counter Automata are Finite State Automata which include a set of registers containing natural numbers, and where state transitions occur based on these register values. The contribution of our work is to extend previous work on verification of counter automata properties to cover arbitrary computable functions and predicates (in principle). In order to achieve this, we use the dependently typed language Agda to verify properties. The advantage of this approach is that it allows us to verify both functional and extra-functional properties such as resource consumption, in the presence of iteration and control parameters. However, we are not able to achieve fully automatic verification. We illustrate our approach using three examples: i) verifying that a particular finite state automaton accepts exactly those binary sequences divisible by 3, if they are interpreted as numbers; ii) verifying the worst-case execution time of a system of three boxes, depending on an unknown control parameter; and iii) verifying the number of box executions for a system of two boxes, which is non-linear.