Implicit data structures for logic and stochastic systems analysis

ABSTRACT

Both logic and stochastic analysis have strong theoretical underpinnings, but they have been traditionally relegated to separate areas of computer science, the former focusing on logic and discrete algorithms, the latter on exact or approximate numerical methods. In the last few years, though, there has been a convergence of research in these two areas, due to the realization that data structures used in one area can benefit the other and that, by merging the goals of the two areas, a more integrated approach to system analysis can be derived. In this paper, we describe some of the beneficial interactions between the two, and some of the research challenges ahead.

REFERENCES

• 1: Adnan Aziz , Kumud Sanwal , Vigyan Singhal , Robert Brayton, Model-checking continuous-time Markov chains, ACM Transactions on Computational Logic (TOCL), v.1 n.1, p.162-170, July 2000 [doi>10.1145/343369.343402]
• 2: C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. Model checking algorithms for continuous-time Markov chains. IEEE TSE, 29(6):524--541, June 2003.
• 3: Marius Bozga , Oded Maler, On the Representation of Probabilities over Structured Domains, Proceedings of the 11th International Conference on Computer Aided Verification, p.261-273, July 06-10, 1999
• 4: 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]
• 5: Peter Buchholz, An Adaptive Decomposition Approach for the Analysis of Stochastic Petri Nets, Proceedings of the 2002 International Conference on Dependable Systems and Networks, p.647-656, June 23-26, 2002
• 6: Peter Buchholz , Gianfranco Ciardo , Susanna Donatelli , Peter Kemper, Complexity of Memory-Efficient Kronecker Operations with Applications to the Solution of Markov Models, INFORMS Journal on Computing, v.12 n.3, p.203-222, July 2000 [doi>10.1287/ijoc.12.3.203.12634]
• 7: P. Buchholz, J. P. Katoen, P. Kemper, and C. Tepper. Model-checking large structured Markov chains. JLAP, 56(1/2):69--97, 2003.
• 8: P. Buchholz , P. Kemper, Numerical analysis of stochastic marked graph nets, Proceedings of the Sixth International Workshop on Petri Nets and Performance Models, p.32, October 03-06, 1995
• 9: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 10: Gianfranco Ciardo , Gerald Lüttgen , Radu Siminiceanu, Saturation: An Efficient Iteration Strategy for Symbolic State-Space Generation, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.328-342, April 02-06, 2001
• 11: Gianfranco Ciardo , Andrew S. Miner, A Data Structure for the Efficient Kronecker Solution of GSPNs, Proceedings of the The 8th International Workshop on Petri Nets and Performance Models, p.22, September 08-10, 1999
• 12: Gianfranco Ciardo , Radu Siminiceanu, Using Edge-Valued Decision Diagrams for Symbolic Generation of Shortest Paths, Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, p.256-273, November 06-08, 2002
• 13: G. Ciardo and R. Siminiceanu. Structural symbolic CTL model checking of asynchronous systems. In Proc. CAV, LNCS 2725, pages 40--53, July 2003. Springer-Verlag.
• 14: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 15: M. Davio. Kronecker products and shuffle algebra. IEEE TC, C-30:116--125, Feb. 1981.
• 16: Daniel D. Deavours , William H. Sanders, "On-the-fly" Soltuion Techniques for Stochastic Petri Nets and Extensions, Proceedings of the 6th International Workshop on Petri Nets and Performance Models, p.132, June 02-06, 1997
• 17: S. Derisavi, P. Kemper, and W. H. Sanders. Symbolic state-space exploration and numerical analysis of state-sharing composed models. Linear Algebra and Its Applications, 386C:137--166, 2004.
• 18: Susanna Donatelli, Superposed Generalized Stochastic Petri Nets: Definition and Efficient Solution, Proceedings of the 15th International Conference on Application and Theory of Petri Nets, p.258-277, June 20-24, 1994
• 19: Paulo Fernandes , Brigitte Plateau , William J. Stewart, Efficient descriptor-vector multiplications in stochastic automata networks, Journal of the ACM (JACM), v.45 n.3, p.381-414, May 1998 [doi>10.1145/278298.278303]
• 20: H. Hermanns, J. Meyer-Kayser, and M. Siegle. Multi terminal binary decision diagrams to represent and analyse continuous-time Markov chains. In Proc. NSMC, pages 188--207, Sept. 1999. Prensas Universitarias de Zaragoza, Spain.
• 21: T. Kam, T. Villa, R. Brayton, and A. Sangiovanni-Vincentelli. Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic, 4(1--2):9--62, 1998.
• 22: Peter Kemper, Numerical Analysis of Superposed GSPNs, IEEE Transactions on Software Engineering, v.22 n.9, p.615-628, September 1996 [doi>10.1109/32.541433]
• 23: Marta Kwiatkowska , Gethin Norman , David Parker, Probabilistic symbolic model checking with PRISM: a hybrid approach, International Journal on Software Tools for Technology Transfer (STTT), v.6 n.2, p.128-142, August 2004 [doi>10.1007/s10009-004-0140-2]
• 24: Andrew S. Miner, Efficient State Space Generation of GSPNs using Decision Diagrams, Proceedings of the 2002 International Conference on Dependable Systems and Networks, p.637-646, June 23-26, 2002
• 25: Andrew S. Miner, Saturation for a General Class of Models, Proceedings of the The Quantitative Evaluation of Systems, First International Conference on (QEST'04), p.282-291, September 27-30, 2004 [doi>10.1109/QEST.2004.38]
• 26: Andrew S. Miner , Gianfranco Ciardo, Efficient Reachability Set Generation and Storage Using Decision Diagrams, Proceedings of the 20th International Conference on Application and Theory of Petri Nets, p.6-25, June 21-25, 1999
• 27: Andrew S. Miner , Gianfranco Ciardo , Susanna Donatelli, Using the exact state space of a Markov model to compute approximate stationary measures, Proceedings of the 2000 ACM SIGMETRICS international conference on Measurement and modeling of computer systems, p.207-216, June 18-21, 2000, Santa Clara, California, United States
• 28: Brigitte Plateau, On the stochastic structure of parallelism and synchronization models for distributed algorithms, Proceedings of the 1985 ACM SIGMETRICS conference on Measurement and modeling of computer systems, p.147-154, August 1985, Austin, Texas, United States
• 29: A. Pnueli. The temporal logic of programs. In Proc. FOCS, pages 46--57. IEEE CS Press, Nov. 1977.

INDEX TERMS

Primary Classification:
  H. Information Systems
  H.1 MODELS AND PRINCIPLES
      H.1.1 Systems and Information Theory
          Subjects: General systems theory

Additional Classification:
  E. Data
  E.1 DATA STRUCTURES

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

  G. Mathematics of Computing
  G.3 PROBABILITY AND STATISTICS
      Subjects: Stochastic processes

General Terms:
Algorithms, Performance