Online minimization of transition systems (extended abstract)

ABSTRACT

We are given a transition system implicitly through a compact representation and wish to perform simultaneously reachability analysis and minimization without constructing first the whole system graph. We present an algorithm for this problem that applies to general systems, provided we have appropriate primitive operations for manipulating blocks of states and we can determine termination; the number of operations needed to construct the minimal reachable graph is quadratic in the size of this graph. We specialize the method to obtain efficient algorithms for extended finite state machines that apply separable affine transformations on the variables.

REFERENCES

• ACD: Alur, R., Courcoubetis, C., and Dill, D. {1990}. Model Checking for Real Time Systems, in Proc. 5th IEEE LICS.
• BFH: Ahmed Bouajjani , Jean-Claude Fernandez , Nicolas Halbwachs, Minimal Model Generation, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.197-203, June 18-21, 1990
• BFHRR: Bouajjani, A., Fernandez, J-C., Halbwachs, N., Raymond, P. and Rat~l, C. {1991}. Minimal State Graph Generation, IMAG Grenoble Preprint.
• Br: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• BD: S. Budkowski , P. Dembinski, An introduction to Estelle: a specification language for distributed systems, Computer Networks and ISDN Systems, v.14 n.1, p.3-23, March, 1987 [doi>10.1016/0169-7552(87)90084-5]
• BCMDH: Burch, J, R., Clarke, E. M., McMillan, K. L., Dill, D. L., and Hwang, L. J. {1990}. Symbolic Model Checking: 102o States and Beyond, in Proc. 5th IEEE LICS, pp. 428-439.
• CES: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• CM: Edith Cohen , Nimrod Megiddo, Improved algorithms for linear inequalities with two variables per inequality, Proceedings of the twenty-third annual ACM symposium on Theory of computing, p.145-155, May 05-08, 1991, New Orleans, Louisiana, United States [doi>10.1145/103418.103438]
• CBM: O. Coudert , C. Berthet , J. C. Madre, Verification of synchronous sequential machines based on symbolic execution, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.365-373, February 1990, Grenoble, France
• CVWY: Costas Courcoubetis , Moshe Y. Vardi , Pierre Wolper , Mihalis Yannakakis, Memory Efficient Algorithms for the Verification of Temporal Properties, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.233-242, June 18-21, 1990
• GS: Susanne Graf , Bernhard Steffen, Compositional Minimization of Finite State Systems, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.186-196, June 18-21, 1990
• HN: Hochbaum, D.S. and Naor, J. {1991}. Simple and Fast Algorithms for Linear and Integer Programs with Two Variables Per Inequality, manuscript.
• Ho1: Gerard J. Holzmann, An improved protocol reachability analysis technique, Software—Practice & Experience, v.18 n.2, p.137-161, Feb., 1988 [doi>10.1002/spe.4380180203]
• Ho2: Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• Hp: Hopcroft, J. E. {1971}. An n log n Algorithm for Minimizing States in a Finite Automaton, in Theory of Machines and Computations, Z. Kohavi and A. Paz (eds.), pp. 189-196, Academic Press, New York.
• JJ: C. Jard , T. Jeron, On-line model checking for finite linear temporal logic specifications, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.189-196, February 1990, Grenoble, France
• KS: Paris C. Kanellakis , Scott A. Smolka, CCS expressions finite state processes, and three problems of equivalence, Information and Computation, v.86 n.1, p.43-68, May 1990 [doi>10.1016/0890-5401(90)90025-D]
• LLC: Logical Link Control {1989}. International Standard ISO 8802-2, IEEE Std. 802.2, The Institute of Electrical and Electronics Engineers, Inc.
• PT: Robert Paige , Robert E. Tarjan, Three partition refinement algorithms, SIAM Journal on Computing, v.16 n.6, p.973-989, December 1, 1987 [doi>10.1137/0216062]
• Pn: A Pnueli, Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends, Current trends in concurrency. Overviews and tutorials, Springer-Verlag New York, Inc., New York, NY, 1986
• SL: Deepinder P. Sidhu , Ting-kau Leung, Formal Methods for Protocol Testing: A Detailed Study, IEEE Transactions on Software Engineering, v.15 n.4, p.413-426, April 1989 [doi>10.1109/32.16602]
• Si: Sifakis, J. {1982}. A Unified Approach for Studying the Properties of Transition Systems, in Theoretical Computer Science3.
• VW: Vardi, M. Y. and Wolper, P. {1986}. An Automata-Theoretic Approach to Automatic Program Verification, in Proc. LICS, pp. 322- 331.
• W: West, C. H. {1978} Generalized Technique for Communication Protocol Validation, in IBM J. Res. andDevel., vol. 22, pp. 393-404.
• YL: Mihalis Yannakakis , David Lee, Testing finite state machines, Proceedings of the twenty-third annual ACM symposium on Theory of computing, p.476-485, May 05-08, 1991, New Orleans, Louisiana, United States [doi>10.1145/103418.103468]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Computations on discrete structures

Additional Classification:
  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

General Terms:
Algorithms, Performance, Theory