Richard Raimi
Abstract
In this paper we outline a theory for the environment-modeling problem, the problem of abstracting component finite state machines (FSMs)bordering a particular FSM of interest within a network of interacting FSMs. The goal is to lay a theoretical foundation for the automatic state reduction of large FSM networks. We feel this is a prerequisite for the efficient use of many verification techniques. We focus on computing conditions for the safe removal of a component FSM in a FSM network, where removal is safe if it preserves a certain well-defined trace equivalence. We present an optimized algorithm for determining language universality of a FSM, as well as determining independence of a FSM from those of its inputs connected to outputs of neighboring FSMs. These two properties, input independence and language universality, provide the necessary and sufficient conditions for safe removal. In addition, we show how simulation relations can be utilized, both to reduce the cost of computing safe removal and to create an appropriate abstract FSM when safe removal is not possible.
- BOUAIJANI, A., FERNANDEZ, J., AND HALBWACHS, N. 1990. Minimal model generation. In Proceedings of the 2nd International Conference on Computer Aided Verification (CAV, New Brunswick, NJ, June), Springer Lecture Notes in Computer Science, vol. 531. Springer-Verlag, Berlin, Germany. Google Scholar
- CLARKE, E. M., EMERSON, E. A., AND SISTLA, A. P. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8, 2 (Apr. 1986), 244-263. Google ScholarDigital Library
- FERNANDEZ, J. C., KERBRAT, A., AND MOUNIER, L. 1993. Symbolic equivalence checking. In Proceedings of the Conference on Computer Aided Verification (CAV '93), C. Courcoubetis, Ed. Springer Lecture Notes in Computer Science, vol. 697. Springer-Verlag, Vienna, Austria. Google Scholar
- HOJATI, R. 1996. A BDD-based environment for formal verification of hardware systems. Ph.D. Dissertation. Department of Electrical Engineering and Computer Science, Univ. of Carlifornia at Berkeley, Berkeley, CA. Google Scholar
- HOPCROFT, J. AND ULLMAN, J. 1979. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading, MA. Google Scholar
- KOENIG, D. 1990. Theory of Finite and Infinite Graphs. Birkh user Boston Inc., Cambridge, MA. Google Scholar
- KURSHAN, R. P. 1990. Analysis of discrete event coordination. In Proceedings of the REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness (Mook, The Netherlands, May 29-June 2), J. W. de Bakker, W. P. de Roever, and G. Rozenberg, Eds. Springer Lecture Notes in Computer Science Springer-Verlag, New York, NY, 414-453. Google Scholar
- LIN, B. AND NEWTON, A. R. 1991. Efficient symbolic manipulation of equivalence relations and classes. In Proceedings of the International Workshop on Formal Methods in VLSI Design (Jan. 1991),Google Scholar
- LONG, D. E. 1993. Model checking, abstraction, and compositional verification. Ph.D. Dissertation. Computer Science Department, Carnegie Mellon University, Pittsburgh, PA. Google Scholar
- MARTIN, A., KAUFMAN, M., AND PIXLEY, C. 1998. Design constraints in symbolic model checking. In Proceedings of the Conference on Computer Aided Verification, Google Scholar
- MEYER, A. AND STOCKMEYER, L. 1972. The equivalence problem for regular expressions with squaring requires exponential time. In Proceedings of the 13th Annual Symposium on Switching and Automata Theory,Google Scholar
- MILNER, R. 1971. An algebraic definition of simulation between programs. In Proceedings of the Second International Joint Conference on Artificial Intelligence, British Computer Society, Swinton, UK, 481-489.Google Scholar
- RAIMI, R. AND HOJATI, R. 1997. Universal finite state machines and environment modeling. In Proceedings of the International Workshop on Logic Synthesis,Google Scholar
- PRASAD SISTLA, A., VARDI, M. Y., AND WOLPER, P. 1987. The complementation problem for B chi automata with applications to temporal logic. Theor. Comput. Sci. 49, 2,3 (Mar. 1987), 217-237. Google ScholarDigital Library
- WANG, H. AND BRAYTON, R. 1993. Input don't care sequences in fsm networks. In Proceedings of the International Conference on Computer Aided Design, Google Scholar
- WATANABE, Y. AND BRAYTON, R. 1994. State minimization of pseudo non-deterministic fsms. In Proceedings on European Design and Test Conference 94 (Paris, France, Feb. 1994),Google ScholarCross Ref
Index Terms
- Environment modeling and language universality
Recommendations
Solving games via three-valued abstraction refinement
Games that model realistic systems can have very large state-spaces, making their direct solution difficult. We present a symbolic abstraction-refinement approach to the solution of two-player games with reachability or safety goals. Given a ...
Local state space construction for compositional verification of concurrent systems
SPIN 2014: Proceedings of the 2014 International SPIN Symposium on Model Checking of SoftwareLocal state space construction is crucial for efficient compositional verification of local and global properties of concurrent systems. This paper presents such an approach where local state transition models are built by iteratively searching the ...
SAT-based counterexample-guided abstraction refinement
We describe new techniques for model checking in the counterexample-guided abstraction-refinement framework. The abstraction phase "hides" the logic of various variables, hence considering them as inputs. This type of abstraction may lead to "spurious" ...
Comments