Abstract
In this paper, we use knowledge-based control theory to monitor global properties in a distributed system. We control the system to enforce that if a given global property is violated, at least one process knows this fact, and therefore may report it. Our approach uses knowledge properties that are precalculated based on model checking. As local knowledge is not always sufficient to monitor a global property in a concurrent system, we allow adding temporary synchronizations between two or more processes to achieve sufficient knowledge. Since synchronizations are expensive, we aim at minimizing their number using the knowledge analysis.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Apt, K., Francez, N.: Modeling the Distributed Termination Convention of CSP. ACM Trans. Program. Lang. Syst. 6(3), 370–379 (1984)
Basu, A., Bensalem, S., Peled, D., Sifakis, J.: Priority Scheduling of Distributed Systems based on Model Checking. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 79–93. Springer, Heidelberg (2009)
Bensalem, S., Bozga, M., Graf, S., Peled, D., Quinton, S.: Methods for Knowledge Based Controlling of Distributed Systems. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 52–66. Springer, Heidelberg (2010)
Chandy, K., Lamport, L.: Distributed Snapshots: Determining Global States of Distributed Systems. ACM Trans. Comput. Syst. 3(1), 63–75 (1985)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)
Genrich, H.J., Lautenbauch, K.: System Modeling with High-level Petri Nets. Theoretical Computer Science 13, 109–135 (1981)
Graf, S., Peled, D., Quinton, S.: Achieving Distributed Control through Model Checking. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 396–409. Springer, Heidelberg (2010)
Keller, R.M.: Formal Verification of Parallel Programs. Communications of the ACM 19, 371–384 (1976)
Havelund, K., Rosu, G.: Monitoring Java Programs with Java PathExplorer. Electr. Notes Theor. Comput. Sci. 55(2) (2001)
Havelund, K., Rosu, G.: Efficient monitoring of safety properties. STTT 6(2), 158–173 (2004)
Katz, G., Peled, D.: Code Mutation in Verification and Automatic Code Generation. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 435–450. Springer, Heidelberg (2010)
van der Meyden, R.: Common Knowledge and Update in Finite Environment. Information and Computation 140(2), 115–157 (1998)
Orlin, J.: Contentment in Graph Theory: Covering Graphs with Cliques. Indagationes Mathematicae 80(5), 406–424 (1977)
Pérez, J., Corchuelo, R., Toro, M.: An Order-based Algorithm for Implementing Multiparty Synchronization. Concurrency - Practice and Experience 16(12), 1173–1206 (2004)
Thistle, J.G.: Undecidability in Decentralized Supervision. System and Control Letters 54, 503–509 (2005)
Thomas, W.: On the Synthesis of Strategies in Infinite Games. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 1–13. Springer, Heidelberg (1995)
Tripakis, S.: Undecidable Problems of Decentralized Observation and Control on Regular Languages. Information Processing Letters 90(1), 21–28 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Graf, S., Peled, D., Quinton, S. (2011). Monitoring Distributed Systems Using Knowledge. In: Bruni, R., Dingel, J. (eds) Formal Techniques for Distributed Systems. FMOODS FORTE 2011 2011. Lecture Notes in Computer Science, vol 6722. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21461-5_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-21461-5_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21460-8
Online ISBN: 978-3-642-21461-5
eBook Packages: Computer ScienceComputer Science (R0)