Acceleration of timing verification method based on time petri nets
The work
| Authors | Tomohiro Yoneda; Yoshihiro Tohma; Yutaka Kondo |
|---|---|
| Editors | |
| Type | article |
| Year | 1991 |
| Citekey | yoneda1991acceleration |
Where it appeared
| Published in | Systems and Computers in Japan |
|---|---|
| Publisher | Wiley |
| Volume | 22 |
| Issue | 12 |
| Pages | 37--52 |
Identifiers
| DOI | 10.1002/scj.4690221204 |
|---|---|
| ISSN | 0882-1666 |
Access
| Landing page | https://doi.org/10.1002/scj.4690221204 |
|---|
From crossref.
Abstract
AbstractA verification method based on time Petri nets automatically proves the correctness of quantitative timing properties for hard real‐time systems. However, the previously proposed method sometimes takes a very long time or requires considerable memory space to complete verifications. This is because the method generates the whole state space of time Petri nets.This paper proposes an efficient verification method based on the single‐place zero‐reachability problem of time Petri nets, but it may be restricted by given time Petri nets. The single‐place zero‐reachability problem can be solved only by checking whether or not some prescribed transitions can finally fire. This does not require extracting the whole state space of time Petri nets.The method proposed herein: (1) reduces the verification problem to the single‐place zero‐reachability problem of time Petri nets; and (2) generates reduced state space sufficient to check the possibility of the firings of all enabled transitions. This paper also contains an example of verifying a simple LAN protocol and compares the performance of both the proposed method and the previous method.
How it got here
| How it got here | agent via crossref |
|---|---|
| Added | 2026-10-25 03:40 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Cite it as
@article{yoneda1991acceleration,
title = {Acceleration of timing verification method based on time petri nets},
author = {Tomohiro Yoneda and Yoshihiro Tohma and Yutaka Kondo},
year = {1991},
journal = {Systems and Computers in Japan},
publisher = {Wiley},
volume = {22},
number = {12},
pages = {37--52},
issn = {0882-1666},
doi = {10.1002/scj.4690221204},
}
This record lives at https://refs.drheap.org/yoneda1991acceleration/ and will keep doing so.