Abstract
In this paper, we propose a new method of testing concurrent systems by using an artificial intelligence technique: reinforcement learning. In particular, the method verifies the liveness properties given in temporal logic formulas and dynamically controls a target system in runtime monitoring to efficiently reveal possible error against specification. In this control, the learning method accumulates necessary information by monitoring the running system. We built a simulator to evaluate this idea and conducted experiments with simple examples. As a result we showed the effectiveness of this approach for solving the difficult problem of testing the liveness properties of concurrent systems.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge, MA (2000)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in Property Specification for Finite-state Verification. In: The 21st ICSE, pp. 411–420 (1999)
Harel, D.: On Visual Formalism. Comm. of ACM, pp. 514–530 (1988)
Havelund, K., Rosu, G.: Testing Linear Temporal Logic Formulae on Finite Execution Traces. RIACS Technical Report TR 01-08 (2001)
Holzmann, G.: Software Analysis and Model Checking. In: Proc. Computer Aided Verification, pp. 1–16 (2002)
Kim, M., Kannan, S., Lee, I., Sokolsky, O., Viswanathan, M.: Java-MaC: a Run-time Assurance Tool for Java Programs. In: Proc. First Workshop on Runtime Verification (RV 2001), July 2001 (2001)
Lynch, N.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1997)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer, Heidelberg (1992)
Sutton, R.S., Barto, A.G.: Reinforcement Learning: An introduction. MIT Press, Cambridge, MA (1998)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Araragi, T., Cho, S.M. (2007). Checking Liveness Properties of Concurrent Systems by Reinforcement Learning. In: Edelkamp, S., Lomuscio, A. (eds) Model Checking and Artificial Intelligence. MoChArt 2006. Lecture Notes in Computer Science(), vol 4428. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74128-2_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-74128-2_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74127-5
Online ISBN: 978-3-540-74128-2
eBook Packages: Computer ScienceComputer Science (R0)