핵심 개념
The paper introduces regular abstraction frameworks, a generalization of the approach to regular model checking based on inductive invariants. It shows that the problem of deciding if the language of the automaton recognizing an overapproximation of the reachable configurations intersects a given regular set of unsafe configurations is EXPSPACE-complete. The paper also presents a learning algorithm that computes this automaton in a lazy manner, stopping whenever the current hypothesis is already strong enough to prove safety.
초록
The paper introduces regular abstraction frameworks, a generalization of the approach to regular model checking based on inductive invariants. Regular abstraction frameworks consist of a regular language of constraints and an interpretation that assigns to each constraint the set of configurations of the regular transition system (RTS) satisfying it. Examples of regular abstraction frameworks include the formulas of previous work, octagons, bounded difference matrices, and views.
The paper shows that the generalization of the decision problem to regular abstraction frameworks remains in EXPSPACE, and proves a matching EXPSPACE-hardness bound. This implies that, in the worst case, the automaton recognizing the overapproximation of the reachable configurations has a double-exponential number of states.
To address this, the paper introduces a learning algorithm that computes this automaton in a lazy manner, stopping whenever the current hypothesis is already strong enough to prove safety. The algorithm involves solving the separability problem: given a pair of configurations, is there an inductive constraint that separates them? The paper shows that this problem is PSPACE-complete and NP-complete for length-preserving interpretations.
The experimental results show that the learning-based approach outperforms the previous approach.
통계
The paper does not provide any specific numerical data or statistics. It focuses on theoretical results regarding the complexity of the abstract safety problem and the design of a learning-based algorithm.
인용구
"Regular transition systems (RTS) are a popular formalism for modelling infinite-state systems satisfying the following conditions: configurations can be encoded as words, the set of initial configurations is recognised by a finite automaton, and the transition relation is recognised by a transducer."
"Regular abstraction frameworks are a formalism to model a wide range of abstractions. An abstraction framework is a triple F = (C, A, V), where C is a set of configurations, A is a set of constraints, and V ⊆A × C is an interpretation."
"EXPSPACE-hardness implies that, in the worst case, the automaton recognising the overapproximation of the reachable configurations has a double-exponential number of states."