Language Inclusion Checking of Timed Automata Based on Property Patterns
The language inclusion checking of timed automata is described as the following: given two timed automata <i>M</i> and <i>N</i>, where <i>M</i> is a system model and <i>N</i> is a specification model (which represents the properties that the system nee...
| Main Authors: | , , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2022-12-01
|
| Series: | Applied Sciences |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2076-3417/12/24/12946 |
| _version_ | 1797461596644048896 |
|---|---|
| author | Ting Wang Yan Shen Tieming Chen Baiyang Ji Tiantian Zhu Mingqi Lv |
| author_facet | Ting Wang Yan Shen Tieming Chen Baiyang Ji Tiantian Zhu Mingqi Lv |
| author_sort | Ting Wang |
| collection | DOAJ |
| description | The language inclusion checking of timed automata is described as the following: given two timed automata <i>M</i> and <i>N</i>, where <i>M</i> is a system model and <i>N</i> is a specification model (which represents the properties that the system needs to satisfy), check whether the language of <i>M</i> is included in the language of <i>N</i>. The language inclusion checking of timed automata can detect whether a system model satisfies a given property under the time constraints. There exist excellent studies on verifying real-time systems using timed automata. However, there is no thorough method of timed automata language inclusion checking for real-life systems. Therefore, this paper proposes a language inclusion checking method of timed automata based on the property patterns. On the one hand, we summarize commonly used property patterns described by timed automata, which can guide people to model the properties with time constraints. On the other hand, the system model <i>M</i> often contains a large number of events, but in general, the property <i>N</i> only needs to pay attention to the sequences and time limits of a few events. Therefore, the timed automata language inclusion checking algorithm is improved so that only the concerned events are required. Our method is applied to a water disposal system and it is also evaluated using benchmark systems. The determinization problem of timed automata is undecidable, which may lead to an infinite state space. However, our method is still practical because the properties established according to property patterns are often deterministic. |
| first_indexed | 2024-03-09T17:22:38Z |
| format | Article |
| id | doaj.art-f970b381febb45bd8e30ad0b7f3fc867 |
| institution | Directory Open Access Journal |
| issn | 2076-3417 |
| language | English |
| last_indexed | 2024-03-09T17:22:38Z |
| publishDate | 2022-12-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Applied Sciences |
| spelling | doaj.art-f970b381febb45bd8e30ad0b7f3fc8672023-11-24T13:07:30ZengMDPI AGApplied Sciences2076-34172022-12-0112241294610.3390/app122412946Language Inclusion Checking of Timed Automata Based on Property PatternsTing Wang0Yan Shen1Tieming Chen2Baiyang Ji3Tiantian Zhu4Mingqi Lv5College of Computer Science, Zhejiang University of Technology, Hangzhou 310023, ChinaCollege of Computer Science, Zhejiang University of Technology, Hangzhou 310023, ChinaCollege of Computer Science, Zhejiang University of Technology, Hangzhou 310023, ChinaCollege of Computer Science, Zhejiang University of Technology, Hangzhou 310023, ChinaCollege of Computer Science, Zhejiang University of Technology, Hangzhou 310023, ChinaCollege of Computer Science, Zhejiang University of Technology, Hangzhou 310023, ChinaThe language inclusion checking of timed automata is described as the following: given two timed automata <i>M</i> and <i>N</i>, where <i>M</i> is a system model and <i>N</i> is a specification model (which represents the properties that the system needs to satisfy), check whether the language of <i>M</i> is included in the language of <i>N</i>. The language inclusion checking of timed automata can detect whether a system model satisfies a given property under the time constraints. There exist excellent studies on verifying real-time systems using timed automata. However, there is no thorough method of timed automata language inclusion checking for real-life systems. Therefore, this paper proposes a language inclusion checking method of timed automata based on the property patterns. On the one hand, we summarize commonly used property patterns described by timed automata, which can guide people to model the properties with time constraints. On the other hand, the system model <i>M</i> often contains a large number of events, but in general, the property <i>N</i> only needs to pay attention to the sequences and time limits of a few events. Therefore, the timed automata language inclusion checking algorithm is improved so that only the concerned events are required. Our method is applied to a water disposal system and it is also evaluated using benchmark systems. The determinization problem of timed automata is undecidable, which may lead to an infinite state space. However, our method is still practical because the properties established according to property patterns are often deterministic.https://www.mdpi.com/2076-3417/12/24/12946timed automatalanguage inclusionproperty patternverification |
| spellingShingle | Ting Wang Yan Shen Tieming Chen Baiyang Ji Tiantian Zhu Mingqi Lv Language Inclusion Checking of Timed Automata Based on Property Patterns Applied Sciences timed automata language inclusion property pattern verification |
| title | Language Inclusion Checking of Timed Automata Based on Property Patterns |
| title_full | Language Inclusion Checking of Timed Automata Based on Property Patterns |
| title_fullStr | Language Inclusion Checking of Timed Automata Based on Property Patterns |
| title_full_unstemmed | Language Inclusion Checking of Timed Automata Based on Property Patterns |
| title_short | Language Inclusion Checking of Timed Automata Based on Property Patterns |
| title_sort | language inclusion checking of timed automata based on property patterns |
| topic | timed automata language inclusion property pattern verification |
| url | https://www.mdpi.com/2076-3417/12/24/12946 |
| work_keys_str_mv | AT tingwang languageinclusioncheckingoftimedautomatabasedonpropertypatterns AT yanshen languageinclusioncheckingoftimedautomatabasedonpropertypatterns AT tiemingchen languageinclusioncheckingoftimedautomatabasedonpropertypatterns AT baiyangji languageinclusioncheckingoftimedautomatabasedonpropertypatterns AT tiantianzhu languageinclusioncheckingoftimedautomatabasedonpropertypatterns AT mingqilv languageinclusioncheckingoftimedautomatabasedonpropertypatterns |