وارسی نمادین گزاره‌های منطق زمانی فازی روی گراف برنامه فازی
الموضوعات :غلامرضا ستوده 1 , علی موقر رحیم‌آبادی 2
1 - دانشگاه آزاد اسلامي، واحد علوم تحقيقات
2 - دانشگاه صنعتي شريف
الکلمات المفتاحية: وارسی مدل مدل کریپکه منطق زمانی فازی گراف برنامه فازی وارسی نمادین مدل,
ملخص المقالة :
با ترکیب منطق‌های زمانی و منطق فازی می‌توان منطق‌های جدیدی ایجاد و از آن در وارسی خودکار مدل‌های پویای فازی استفاده نمود. تاکنون در چند مقاله مدل‌های کریپکه فازی FzKripke و گراف برنامه فازی FzPG به عنوان دو مدل زمانی فازی تعریف و جهت وارسی خواص زمانی روی این مدل‌ها، منطق زمانی FzCTL ارائه شده و بدون ارائه الگوریتم وارسی مدل، کاربردهایی از آنها در وارسی مدارات منطقی فازی مانند فلیپ- فلاپ‌های فازی معرفی شده است. در این مقاله جهت برخورد با مشکل انفجار فضای حالت در مدل‌های زمانی فازی، روشی نمادین ارائه شده که به کمک آن، مدل‌ها در قالبی بسیار فشرده ذخیره و پردازش می‌شوند. در این مقاله کارایی الگوریتم‌های طراحی‌شده نیز مورد ارزیابی تحلیلی و تجربی قرار می‌گیرند. به عنوان مطالعه موردی، کارایی روش در وارسی و کشف مخاطره پویای یک مدار فلیپ- فلاپ D فازی، مورد بررسی قرار گرفته و زمان اجرا و حافظه مصرفی الگوریتم در شرایط مختلف مدل، ارائه شده است
[1] E. M. Clarke, J. O. Grumberge, and D. A. Peled, Model Checking, Cambridge, MA: MIT Press, 1999.
[2] C. Baier and J. P. Katoen, Priciples of Model Checking, Cambridge, MA: MIT Press, 2008.
[3] M. Huth and M. Ryan, Logic Computer Science, 2nd Ed. New York: Cambridge Univ. Press, 2004.
[4] B. Konikowska and W. Penczek, "On designated values in multi-valued CTL* model checking," Fundamenta Informaticae, vol. 60, no. 1-4, pp. 211-224, Sept. 2003.
[5] M. Kwiatkowska, G. Norman, J. Sproston, and J. Wang, "Symbolic model checking for probabilistic timed automata," Information and Computation, vol. 205, no. 7, pp. 1027-1077, Jul. 2007.
[6] F. Wang, Symbolic Implementation of Model-Checking Probabilistic Timed Automata, Ph.D Dissertation, School of Comput. Sci., Univ. of Birmingham, UK, 2006.
[7] F. Wang and M. Kwiatkowska, "An MTBDD-based implementation of forward reachability for probabilistic timed automata," in Proc. 3rd Int. Sym. on Automated Technology for Verification and Analysis, ATVA'05, pp. 385-399, Oct. 2005.
[8] M. Chechik, B. Devereux, S. Easterbrook, and A. Gurfinkel, "Multi-valued symbolic model-checking," ACM Trans. Softw. Eng. Methodol., vol. 12, no. 4, pp. 371-408, Oct. 2003.
[9] M. Chechik, S. Easterbrook, and V. Petrovykh, "Model-checking over multi-valued logics," in Proc. Int. Symp. Formal Methods Europe on Formal Methods for Increasing Software Productivity, FME'01, pp. 72-98, Berlin, Germany, Mar. 2001.S [10] M. Chechik, A. Gurfinkel, B. Devereux, A. Lai, and S. Easterbrook, "Data structures for symbolic multi-valued model-checking," Form. Method Syst. Des., vol. 29, no. 3, pp. 295-344, Nov. 2006.
[11] G. E. Fainekos, An Introduction to Multi-Valued Model Checking, Dept. Computer and Information Science, Univ. of Pennsylvania, Tech. Rep. MS-CIS-05-16, 2005.
[12] A. Gurfinkel, Multi-Valued Symbolic Model-Checking: Fairness, Counter-Examples, Running Time, M.S Thesis, Dept. Comput. Sci., Univ. of Toronto, Canada, 2003.
[13] A. F. Vilas, J. J. P. Arias, A. B. B. Martınez, M. L. Nores, R. P. D. Redondo, A. G. Solla, J. G. Duque, and M. R. Cabrer, "Multi-valued model checking in dense-time," Lecture Notes in Computer Science, vol. 3751, pp. 638-649, Dec. 2005.
[14] H. Pan, Y. Li, Y. Cao, and Z. Ma, "Model checking computation tree logic over finite lattices," Theoretical Computer Science, vol. 612, pp. 45-62, Jan. 2016.
[15] N. Sladoje, On Analysis of Discrete Spatial Fuzzy Sets in 2 and 3 Dimensions, Ph.D. Dissertation, Centre for Image Analysis, SLU and Uppsala Univ., Uppsala, Sweden, 2005.
[16] M. J. Wierman, An Introduction to the Mathematics of Uncertainty, 1st. ed., 20 Aug. 2010.
[17] P. Carinena, A. Burgarin, M. Mucientes, and S. Barro, "A language for expressing expert knowledge using fuzzy temporal rules," in Proc. EUSFLAT-ESTYLF Joint Conf., pp. 171-174, Palma de Mallorca, Spain, Sept. 1999.
[18] S. Moon, K. Lee, and D. Lee, "Fuzzy branching temporal logic," IEEE Trans. Syst. Man Cybern. B, vol. 34, no. 2, pp. 1045-1055, Sept. 2004.
[19] J. Whittle, P. Sawyer, N. Bencomo, B. H. C. Cheng, and J. M. Bruel, "RELAX: incorporating uncertainty into the specification of self-adaptive systems," in Proc. 17th IEEE Int. Requirements Eng. Conf,. RE'09, pp. 79-88, Atlanta, GA, USA, Apr. 2009.
[20] G. Palshikar, "Representing fuzzy temporal knowledge," in Proc. Int. Conf. on Knowledge-Based Systems, KBCS'00, pp. 252-263, Mumbai, India, Dec. 2000.
[21] G. Bruns and P. Godefroid, "Model checking with multi-valued logics," Lecture Notes in Computer Science, vol. 3142, pp. 281-293, Jul. 2004.
[22] B. Intrigila, D. Magazzeni, A. Tofani, I. Melatti, and E. Tronci, "A model checking technique for the verification of fuzzy control systems," in Proc. Int. Conf. on Computational Intell. for Modelling, Control and Automation and Int. Conf. on Intelligent Agents, Web Tech. and Internet Commerce, vol. 2, pp. 536-542, Nov. 2005.
[23] W. Liang, W. Bing-Wen, and G. Yi-Ping, "Cell mapping description for digital control system with quantization effect," presented at Computing Research Repository, CoRR, 2007, http://arxiv.org/abs/0712.2501
[24] J. Y. Yen and S. W. Tarng, "A fuzzy cell-mapping feedback control algorithm for the satellite attitude maneuvering control," in Proc. Asian Fuzzy Syst. Symp. Soft Computing in Intelligent Syst. and Inform. Process., pp. 567-572, Kenting, Taiwan, Dec. 1996.
[25] غ. ر. ستوده و ع. موقر رحیم‌آبادی، "تقریب و تجدید در منطق و مدل‌های زمانی فازی"، شانزدهمین کنفرانس بین‌المللی سالانه انجمن کامپیوتر ایران، صص. 166-160، تهران، اسفند ۱۳۸۹.
[26] G. R. Sotudeh and A. Movaghar, "Abstraction and approximation in fuzzy temporal logics and models," Formal Aspects of Computing, London, UK, Springer-Verlag, vol. 27, no. 2, pp. 309-334, Mar. 2015.
[27] G. R. Sotudeh and A. Movaghar, "Applications of fuzzy program graph in symbolic checking of fuzzy flip-flops," J. of Computer & Robotics, vol. 7, no. 1, pp. 22-36, Winter/Spring 2014.
[28] H. Pan, Y. Li, Y. Cao, and Z. Ma, "Model checking fuzzy computation tree logic," Fuzzy Sets and Systems, vol. 262, pp. 60-77, Mar. 2015.
[29] غ. ر. ستوده و ع. موقر رحیم‌آبادی، "تعمیم مدل و منطق زمانی فازی به زمان حقیقی،" مجموعه مقالات هفدهمین کنفرانس سالانه انجمن کامپیوتر ایران، تهران، صص. 524-517، اسفند 1390.
[30] S. Mukherjee and P. Dasgupta, "A fuzzy real-time temporal logic," International J. of Approximate Reasoning, vol. 54, no. 9, pp. 1452-1470, Nov. 2013.
[31] J. Nild-Nielson, BuDDy-A Binary Decision Diagram Package, Dep. Inform. Tech., Technical Univ. of Denmark, 1999.
[32] http://nusmv.fbk.eu
[33] B. Choi and K. Shukla, "Multi-valued logic circuit design and implementation," International J. of Electronics and Electrical Engineering, vol. 3, no. 4, pp. 256-262, Aug. 2015.
