Abstraction and approximation in fuzzy temporal logics and models

Verfasser / Beitragende:
[Gholamreza Sotudeh, Ali Movaghar]
Ort, Verlag, Jahr:
2015
Enthalten in:
Formal Aspects of Computing, 27/2(2015-03-01), 309-334
Format:
Artikel (online)
ID: 605516391
LEADER caa a22 4500
001 605516391
003 CHVBK
005 20210128100714.0
007 cr unu---uuuuu
008 210128e20150301xx s 000 0 eng
024 7 0 |a 10.1007/s00165-014-0318-7  |2 doi 
035 |a (NATIONALLICENCE)springer-10.1007/s00165-014-0318-7 
245 0 0 |a Abstraction and approximation in fuzzy temporal logics and models  |h [Elektronische Daten]  |c [Gholamreza Sotudeh, Ali Movaghar] 
520 3 |a Recently, by defining suitable fuzzy temporal logics, temporal properties of dynamic systems are specified during model checking process, yet a few numbers of fuzzy temporal logics along with capable corresponding models are developed and used in system design phase, moreover in case of having a suitable model, it suffers from the lack of a capable model checking approach. Having to deal with uncertainty in model checking paradigm, this paper introduces a fuzzy Kripke model (FzKripke) and then provides a verification approach using a novel logic called Fuzzy Computation Tree Logic* (FzCTL*). Not only state space explosion is handled using well-known concepts like abstraction and bisimulation, but an approximation method is also devised as a novel technique to deal with this problem. Fuzzy program graph, a generalization of program graph and FzKripke, is also introduced in this paper in consideration of higher level abstraction in model construction. Eventually modeling, and verification of a multi-valued flip-flop is studied in order to demonstrate capabilities of the proposed models. 
540 |a British Computer Society, 2014 
690 7 |a Abstraction  |2 nationallicence 
690 7 |a Approximation  |2 nationallicence 
690 7 |a Fuzzy Kripke model  |2 nationallicence 
690 7 |a Fuzzy temporal logic  |2 nationallicence 
690 7 |a Model checking  |2 nationallicence 
690 7 |a Fuzzy program graph  |2 nationallicence 
690 7 |a Multi-valued flip-flop  |2 nationallicence 
700 1 |a Sotudeh  |D Gholamreza  |u Department of Computer Engineering, Islamic Azad University (Science and Research Branch), Tehran, Iran  |4 aut 
700 1 |a Movaghar  |D Ali  |u Department of Computer Engineering, Islamic Azad University (Science and Research Branch), Tehran, Iran  |4 aut 
773 0 |t Formal Aspects of Computing  |d Springer London  |g 27/2(2015-03-01), 309-334  |x 0934-5043  |q 27:2<309  |1 2015  |2 27  |o 165 
856 4 0 |u https://doi.org/10.1007/s00165-014-0318-7  |q text/html  |z Onlinezugriff via DOI 
898 |a BK010053  |b XK010053  |c XK010000 
900 7 |a Metadata rights reserved  |b Springer special CC-BY-NC licence  |2 nationallicence 
908 |D 1  |a research-article  |2 jats 
949 |B NATIONALLICENCE  |F NATIONALLICENCE  |b NL-springer 
950 |B NATIONALLICENCE  |P 856  |E 40  |u https://doi.org/10.1007/s00165-014-0318-7  |q text/html  |z Onlinezugriff via DOI 
950 |B NATIONALLICENCE  |P 700  |E 1-  |a Sotudeh  |D Gholamreza  |u Department of Computer Engineering, Islamic Azad University (Science and Research Branch), Tehran, Iran  |4 aut 
950 |B NATIONALLICENCE  |P 700  |E 1-  |a Movaghar  |D Ali  |u Department of Computer Engineering, Islamic Azad University (Science and Research Branch), Tehran, Iran  |4 aut 
950 |B NATIONALLICENCE  |P 773  |E 0-  |t Formal Aspects of Computing  |d Springer London  |g 27/2(2015-03-01), 309-334  |x 0934-5043  |q 27:2<309  |1 2015  |2 27  |o 165