وارسی نمادین گزاره‌های منطق زمانی فازی روی گراف برنامه فازی
محورهای موضوعی : مهندسی برق و کامپیوترغلامرضا ستوده 1 * , علی موقر رحیم‌آبادی 2
1 - دانشگاه آزاد اسلامي، واحد علوم تحقيقات
2 - دانشگاه صنعتي شريف
کلید واژه: وارسی مدل مدل کریپکه منطق زمانی فازی گراف برنامه فازی وارسی نمادین مدل,
چکیده مقاله :
با ترکیب منطق‌های زمانی و منطق فازی می‌توان منطق‌های جدیدی ایجاد و از آن در وارسی خودکار مدل‌های پویای فازی استفاده نمود. تاکنون در چند مقاله مدل‌های کریپکه فازی FzKripke و گراف برنامه فازی FzPG به عنوان دو مدل زمانی فازی تعریف و جهت وارسی خواص زمانی روی این مدل‌ها، منطق زمانی FzCTL ارائه شده و بدون ارائه الگوریتم وارسی مدل، کاربردهایی از آنها در وارسی مدارات منطقی فازی مانند فلیپ- فلاپ‌های فازی معرفی شده است. در این مقاله جهت برخورد با مشکل انفجار فضای حالت در مدل‌های زمانی فازی، روشی نمادین ارائه شده که به کمک آن، مدل‌ها در قالبی بسیار فشرده ذخیره و پردازش می‌شوند. در این مقاله کارایی الگوریتم‌های طراحی‌شده نیز مورد ارزیابی تحلیلی و تجربی قرار می‌گیرند. به عنوان مطالعه موردی، کارایی روش در وارسی و کشف مخاطره پویای یک مدار فلیپ- فلاپ D فازی، مورد بررسی قرار گرفته و زمان اجرا و حافظه مصرفی الگوریتم در شرایط مختلف مدل، ارائه شده است
We may investigate the correctness of dynamic fuzzy models by a combination of Modal Temporal Logics and Fuzzy Logic. So far Fuzzy-extended Kripke structure (FzKripke) and Fuzzy-extended Program Graph (FzPG) are introduced as two timed Fuzzy logic models. Meanwhile, a Fuzzy-extended Temporal Logic (FzCTL) is introduced. Although no verification technique is devised for verifying FzCTL properties of timed Fuzzy logic models, its applications in verification of Fuzzy Logic Circuits (i.e., Fuzzy Flip-Flops) are studied and elaborated. In this paper we introduce a symbolic approach to tackle the state space explosion problem in timed Fuzzy logic models with which models are simultaneously compressed and processed in the most compact representation possible yet. The applicability of this approach is also demonstrated through experiments on a case study concerning dynamic hazards in a Fuzzy D-Flip Flop. Performance measures like runtime and memory consumptions are also provided for different scenarios.
[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.