Double Depth First Search Based Parametric Analysis for Parametric Time-Interval Automata(<Special Section>Concurrent/Hybrid Systems : Theory and Applications)
スポンサーリンク
概要
- 論文の詳細を見る
In this paper, we propose a parametric model checking algorithm for a subclass of Timed Automata called Parametric Time-Interval Automata (PTIA). In a PTIA, we can specify upper- and lower-bounds of the execution time (time-interval) of each transition using parameter variables. The proposed algorithm takes two inputs, a model described in a PTIA and a property described in a PTIA accepting all invalid infinite/finite runs (called a never claim), or valid finite runs of the model. In the proposed algorithm, firstly we determinize and complement the given property PTIA if it accepts valid finite runs. Secondly, we accelerate the given model, that is, we regard all the actions that are not appeared in the given property PTIA as invisible actions and eliminate them from the model while preserving the set of visible traces and their timings. Thirdly, we construct a parallel composition of the model and the property PTIAs which is accepting all invalid runs that are accepted by the model. Finally, we perform the extension of Double Depth First Search (DDFS), which is used in the automata-theoretic approach to Linear-time Temporal Logic (LTL) model checking, to derive the weakest parameter condition in order that the given model never executes the invalid runs specified by the given property.
- 社団法人電子情報通信学会の論文
- 2005-11-01
著者
-
Hashimoto Hideaki
Graduate School Of Information Science And Technology Osaka University
-
Nakata Akio
Graduate School of Medical Sciences, Kanazawa University
-
Tanimoto Tadaaki
Graduate School Of Information Science And Technology Osaka University
-
Higashino Teruo
Graduate School Of Information Science And Technology Osaka University
-
Nakata Akio
Graduate School Of Information Science And Technology Osaka University
関連論文
- A Contact-based Hybrid Routing Protocol for Mobile Ad Hoc Networks
- Aging Does Not Influence Sympathetic Neurotransmission Property to Arterial Pressure in Humans
- Impaired Sympathetic Nerve Transmission in Heart Failure : Evaluation Using Akaike's Relative Power Contribution Analysis
- A WDS Clustering Algorithm for Wireless Mesh Networks
- An Optical-Drop Wavelength Assignment Algorithm for Efficient Wavelength Reuse under Heterogeneous Traffic in WDM Ring Networks(Discrete Mathematics and Its Applications)
- A Minimum Dead Space Algorithm for Generalized Isochronous Channel Reuse Problems in DQDB Networks(Network)
- P2PMM_router : A Two-Stage Heuristic Algorithm to Peer-to-Peer Multicast Routing Problems in Multihome Networks(Discrete Mathematics and Its Applications)
- A Proposal of Test Sequence Generation Method for Communication Protocols Using SAT Algorithm
- Double Depth First Search Based Parametric Analysis for Parametric Time-Interval Automata(Concurrent/Hybrid Systems : Theory and Applications)
- A Proposal of Improved Lip Contour Extraction Method Using Deformable Template Matching and Its Application to Dental Treatment
- Performance evaluation of vital-sign collection mechanism using wireless sensor device (モバイルマルチメディア通信)
- An Efficient Overlay Multicast Protocol for Heterogeneous Users(Selected Papers from ICMU 2005(Second International Conference on Mobile Computing and Ubiquitous Networking))
- Self-Estimation of Neighborhood Distribution for Mobile Wireless Nodes
- Self-Estimation of Neighborhood Distribution for Mobile Wireless Nodes
- An Efficient Overlay Multicast Protocol for Heterogeneous Users