Top

Published in:

2018 | OriginalPaper | Chapter

Verifying CTL with Unfoldings of Petri Nets

Authors : Lanlan Dong, Guanjun Liu, Dongming Xiang

Published in: Algorithms and Architectures for Parallel Processing

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

There are many studies on verifying Computation Tree Logic (CTL) based on reachable graphs of Petri nets. However, they often suffer from the state explosion problem. In order to avoid/alleviate this problem, we use the unfolding technique of Petri nets to verify CTL. For highly concurrent systems, this technique implicitly represents all reachable states and greatly saves storage space. We construct verification algorithms and develop a related tool. Experiments show the advantages of our method.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Reliable Content Delivery in Lossy Named Data Networks Based on Network Coding

next chapter Deep Q-Learning for Navigation of Robotic Arm for Tokamak Inspection

Dai, Y.Y., Brayton, R.K.: Verification and synthesis of clock-gated circuits. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. PP(99), 1 (2017)

Griggio, A., Roveri, M.: Comparing different variants of the IC3 algorithm for hardware model checking. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 35(6), 1026–1039 (2016)CrossRef

Gnesi S, Margaria T.: Practical applications of probabilistic model checking to communication protocols, pp. 133–150. Wiley-IEEE Press (2013)

Wang, H., Zhao, T., Ren, F., et al.: Integrated modular avionics system safety analysis based on model checking. In: Reliability and Maintainability Symposium, pp. 1–6. IEEE (2017)

Hegde, M.S., Jnanamurthy, H.K., Singh, S.: Modelling and verification of extensible authentication protocol using spin model checker. Int. J. Netw. Secur. Its Appl. 4(6), 81–98 (2012)

Petri, C.A.: Kommunikation mit Automaten. Ph.D. Thesis, Institut Fuer Instrumentelle Mathematik (1962)

Clarke, E.M., Grumberg, O., Hiraishi, H., et al.: Verification of the Futurebus+ cache coherence protocol. Form. Methods Syst. Des. 6, 217–232 (1995)CrossRef

Bryant, R.E., Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)CrossRef

Burch, J.R., et al.: Symbolic model checking: 10 20, states and beyond. Inf. Comput. 98(2), 142–170 (1992)MathSciNetCrossRef

10.

Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. Computer Science Department, pp. 49–58 (1991)

11.

Valmari, A., Hansen, H.: Stubborn set intuition explained. In: Koutny, M., Kleijn, J., Penczek, W. (eds.) Transactions on Petri Nets and Other Models of Concurrency XII. LNCS, vol. 10470, pp. 140–165. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-55862-1_7CrossRef

12.

Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. ACM SIGPLAN Not. 40(1), 110–121 (2005)CrossRef

13.

Boucheneb, H., Barkaoui, K.: Delay-dependent partial order reduction technique for real time systems. Real-Time Syst. 54(2), 278–306 (2018)CrossRef

14.

Si, Y., Sun, J., Liu, Y., Wang, T.: Improving model checking stateful timed CSP with non-zenoness through clock-symmetry reduction. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 182–198. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-41202-8_13CrossRef

15.

Podelski, A., Rybalchenko, A.: ARMC: the logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 245–259. Springer, Heidelberg (2006). https://doi.org/10.1007/978-3-540-69611-7_16CrossRef

16.

Nouri, A., Raman, B., Bozga, M., Legay, A., Bensalem, S.: Faster statistical model checking by means of abstraction and learning. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 340–355. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11164-3_28CrossRef

17.

Liu, G., Reisig, W., Jiang, C., et al.: A branching-process-based method to check soundness of workflow systems. IEEE Access 4, 4104–4118 (2016)CrossRef

18.

Liu, G., Zhang, K., Jiang, C.: Deciding the deadlock and livelock in a petri net with a target marking based on its basic unfolding. In: Carretero, J., Garcia-Blas, J., Ko, R.K.L., Mueller, P., Nakano, K. (eds.) ICA3PP 2016. LNCS, vol. 10048, pp. 98–105. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-49583-5_7CrossRef

19.

Xiang, D., Liu, G., Yan, C., et al.: Detecting data inconsistency based on the unfolding technique of petri nets. IEEE Trans. Ind. Inform. 13, 2995–3005 (2017)CrossRef

20.

Esparza, J., Heljanko, K.: Implementing LTL model checking with net unfoldings. In: Dwyer, M. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 37–56. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45139-0_4CrossRefMATH

21.

Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)

22.

Esparza, J., Vogler, W.: An improvement of McMillan’s unfolding algorithm. LNCS 1099(3), 285–310 (2002)MATH

23.

Himmel, A.S., Molter, H., Niedermeier, R., et al.: Adapting the BronCKerbosch algorithm for enumerating maximal cliques in temporal graphs. Soc. Netw. Anal. Min. 7(1), 35 (2017)

24.

Bonnet-Torrés, O., Domenech, P., Lesire, C., Tessier, C.: Exhost-PIPE: PIPE extended for two classes of monitoring petri nets. In: Donatelli, S., Thiagarajan, P.S. (eds.) ICATPN 2006. LNCS, vol. 4024, pp. 391–400. Springer, Heidelberg (2006). https://doi.org/10.1007/11767589_22CrossRef

25.

Roch, S., Starke, P.H.: INA: Integrated Net Analyzer (2002). https://www2.informatik.hu-berlin.de/~starke/ina.html

Title: Verifying CTL with Unfoldings of Petri Nets
Authors: Lanlan Dong
Guanjun Liu
Dongming Xiang
Publisher: Springer International Publishing
Book: Algorithms and Architectures for Parallel Processing
Print ISBN: 978-3-030-05062-7

Electronic ISBN: 978-3-030-05063-4

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-030-05063-4_5

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner