Checking Liveness Properties of Concurrent Systems by Reinforcement Learning

  • Tadashi Araragi
  • Seung Mo Cho
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4428)


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.


Model Check Response Property Mutual Exclusion Linear Temporal Logic Concurrent System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge, MA (2000)Google Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    Harel, D.: On Visual Formalism. Comm. of ACM, pp. 514–530 (1988)Google Scholar
  4. 4.
    Havelund, K., Rosu, G.: Testing Linear Temporal Logic Formulae on Finite Execution Traces. RIACS Technical Report TR 01-08 (2001)Google Scholar
  5. 5.
    Holzmann, G.: Software Analysis and Model Checking. In: Proc. Computer Aided Verification, pp. 1–16 (2002)Google Scholar
  6. 6.
    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)Google Scholar
  7. 7.
    Lynch, N.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1997)Google Scholar
  8. 8.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer, Heidelberg (1992)Google Scholar
  9. 9.
    Sutton, R.S., Barto, A.G.: Reinforcement Learning: An introduction. MIT Press, Cambridge, MA (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Tadashi Araragi
    • 1
  • Seung Mo Cho
    • 2
  1. 1.NTT Communication Science Laboratories, Nippon Telegraph and Telephone CorporationJapan
  2. 2.Division of Computer Science, Samsung Electronics Co.Korea

Personalised recommendations