article

Implicit data structures for logic and stochastic systems analysis

Authors:

Gianfranco Ciardo,

Andrew S. MinerAuthors Info & Claims

ACM SIGMETRICS Performance Evaluation Review, Volume 32, Issue 4

Pages 4 - 9

https://doi.org/10.1145/1059816.1059818

Published: 01 March 2005 Publication History

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]

A. Aziz, K. Sanwal, V. Singhal, and R. Brayton. Model-checking continuous-time markov chains. ACM Trans. Comput. Logic, 1(1):162--170, 2000.]]

Digital Library

[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.]]

Digital Library

[3]

M. Bozga and O. Maler. On the representation of probabilities over structured domains. In Proc. CAV, LNCS 1633, pages 261--273, July 1999. Springer-Verlag.]]

Digital Library

[4]

R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE TC, 35(8):677--691, Aug. 1986.]]

Digital Library

[5]

P. Buchholz. An adaptive decomposition approach for the analysis of stochastic Petri nets. In Proc. DSN, pages 647--656, June 2002.]]

Digital Library

[6]

P. Buchholz, G. Ciardo, S. Donatelli, and P. Kemper. Complexity of memory-efficient Kronecker operations with applications to the solution of Markov models. INFORMS J. Comp., 12(3):203--222, 2000.]]

[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 and P. Kemper. Numerical analysis of stochastic marked graphs. In Proc. PNPM, pages 32--41, Oct. 1995. IEEE CS Press.]]

Digital Library

[9]

J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98:142--170, 1992.]]

Digital Library

[10]

G. Ciardo, G. Luettgen, and R. Siminiceanu. Saturation: An efficient iteration strategy for symbolic state space generation. In Proc. TACAS, LNCS 2031, pages 328--342, Apr. 2001. Springer-Verlag.]]

Digital Library

[11]

G. Ciardo and A. S. Miner. A data structure for the efficient Kronecker solution of GSPNs. In Proc. PNPM, pages 22--31, Sept. 1999. IEEE CS Press.]]

Digital Library

[12]

G. Ciardo and R. Siminiceanu. Using edge-valued decision diagrams for symbolic generation of shortest paths. In Proc. FMCAD, LNCS 2517, pages 256--273, Nov. 2002. Springer-Verlag.]]

Digital Library

[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]

E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. IBM Workshop on Logics of Programs, LNCS 131, pages 52--71. Springer-Verlag, 1981.]]

Digital Library

[15]

M. Davio. Kronecker products and shuffle algebra. IEEE TC, C-30:116--125, Feb. 1981.]]

[16]

D. D. Deavours and W. H. Sanders. "On-the-fly" solution techniques for stochastic Petri nets and extensions. In Proc. PNPM, pages 132--141, June 1997. IEEE CS Press.]]

Digital Library

[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]

S. Donatelli. Superposed generalized stochastic Petri nets: definition and efficient solution. In Proc. ICATPN, LNCS 815, pages, 258--277, June 1994. Springer-Verlag.]]

Digital Library

[19]

P. Fernandes, B. Plateau, and W. J. Stewart. Efficient descriptor-vector multiplication in stochastic automata networks. JACM, 45(3):381--414, 1998.]]

Digital Library

[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]

P. Kemper. Numerical analysis of superposed GSPNs. IEEE TSE, 22(4):615--628, Sept. 1996.]]

Digital Library

[23]

M. Z. Kwiatkowska, G. Norman, and D. Parker. Probabilistic symbolic model checking with PRISM: a hybrid approach. Software Tools for Technology Transfer, 6(2):128--142, 2004.]]

Digital Library

[24]

A. S. Miner. Efficient state space generation of GSPNs using decision diagrams. In Proc. DSN, pages 637--646, June 2002.]]

Digital Library

[25]

A. S. Miner. Saturation for a general class of models. In Proc. QEST, pages 282--291, Sept. 2004.]]

Digital Library

[26]

A. S. Miner and G. Ciardo. Efficient reachability set generation and storage using decision diagrams. In Proc. ICATPN, LNCS 1639, pages 6--25, June 1999. Springer-Verlag.]]

Digital Library

[27]

A. S. Miner, G. Ciardo, and S. Donatelli. Using the exact state space of a Markov model to compute approximate stationary measures. In Proc. SIGMETRICS, pages 207--216, June 2000.]]

Digital Library

[28]

B. Plateau. On the stochastic structure of parallelism and synchronisation models for distributed algorithms. In Proc. SIGMETRICS, pages 147--153, May 1985.]]

Digital Library

[29]

A. Pnueli. The temporal logic of programs. In Proc. FOCS, pages 46--57. IEEE CS Press, Nov. 1977.]]

Digital Library

Cited By

Thierry-Mieg YPoitrenaud DHamez AKordon F(2009)Hierarchical Set Decision Diagrams and Regular ModelsProceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009,10.1007/978-3-642-00768-2_1(1-15)Online publication date: 27-Mar-2009
https://dl.acm.org/doi/10.1007/978-3-642-00768-2_1

Index Terms

Recommendations

Programming Data Structures in Logic
Stochastic Coalgebraic Logic
Limiting Discounted-Cost Control of Partially Observable Stochastic Systems

This paper presents two main results on partially observable (PO) stochastic systems. In the first one, we consider a general PO system $$ x_{t+1}= F (x_t, a_t, xi_t), , y_t= G(x_t, eta_t) (t=0,1,ldots) hspace{1in} (*) $$ on Borel spaces, with possibly ...

Comments

Information & Contributors

Information

Published In

cover image ACM SIGMETRICS Performance Evaluation Review

ACM SIGMETRICS Performance Evaluation Review Volume 32, Issue 4

March 2005

45 pages

ISSN:0163-5999

DOI:10.1145/1059816

Issue’s Table of Contents

Copyright © 2005 Authors.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 March 2005

Published in SIGMETRICS Volume 32, Issue 4

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
147
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Thierry-Mieg YPoitrenaud DHamez AKordon F(2009)Hierarchical Set Decision Diagrams and Regular ModelsProceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009,10.1007/978-3-642-00768-2_1(1-15)Online publication date: 27-Mar-2009
https://dl.acm.org/doi/10.1007/978-3-642-00768-2_1

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents