Abstraction and approximation in fuzzy temporal logics and models
Gespeichert in:
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)
Online Zugang:
| 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 | ||