Committee |
Date Time |
Place |
Paper Title / Authors |
Abstract |
Paper # |
SS |
2024-03-07 13:30 |
Okinawa |
(Primary: On-site, Secondary: Online) |
Zone-Based Reachability Analysis of Nested Timed Automata Seiichiro Tachi (Nagoya Univ), Mizuhito Ogawa (JAIST), Shoji Yuen (Nagoya Univ) SS2023-53 |
We present a zone-based reachability analysis for Nested Timed Automata (NeTA).
NeTA is a timed pushdown automaton that... [more] |
SS2023-53 pp.25-30 |
NS, SR, RCS, SeMI, RCC (Joint) |
2022-07-15 13:40 |
Ishikawa |
The Kanazawa Theatre + Online (Primary: On-site, Secondary: Online) |
Performance Analysis of a Link Symmetry Confirmation Method in Backoff-based Opportunistic Routing Takuma Yamazaki (SIT), Eri Hosonuma (UT), Taku Yamazaki, Takumi Miyoshi, Thomas Silverston (SIT) NS2022-57 |
Backoff-based opportunistic routing autonomously selects a forwarder based on a random backoff time using hop counts. Ho... [more] |
NS2022-57 pp.147-150 |
VLD, DC, RECONF, ICD, IPSJ-SLDM (Joint) [detail] |
2020-11-17 09:55 |
Online |
Online |
Efficient computation of inductive invariant through flipflop selection Fudong Wang, Masahiro Fujita (U-Tokyo) VLD2020-20 ICD2020-40 DC2020-40 RECONF2020-39 |
As we all know, verification plays more and more important role in VLSI design and manufacture. However, it always takes... [more] |
VLD2020-20 ICD2020-40 DC2020-40 RECONF2020-39 pp.54-59 |
NLP, MSS (Joint) |
2019-03-14 13:45 |
Fukui |
Bunkyo Camp., Univ. of Fukui |
Implementation of Rigorous Simulator for Hybrid Systems Based on Duracz et al. 's Operational Semantics Shota Kojima, Daisuke Ishii (U. Fukui) MSS2018-84 |
Rigorous numerical simulation based on a safe approximation of states plays an important role in analysis of hybrid syst... [more] |
MSS2018-84 pp.19-22 |
MSS, CAS, IPSJ-AL [detail] |
2018-11-12 16:15 |
Shizuoka |
|
A Method for Improving Memory Efficiency of the Reachability Graph Generation Process in General Petri Nets Kohei Fujimori, Yojiro Harie, Katsumi Wasaki (Shinshu Univ.) CAS2018-65 MSS2018-41 |
State space generator is one of the analysis functions of Petri net
design tool HiPS (Hierarchical Petri net Simulator)... [more] |
CAS2018-65 MSS2018-41 pp.43-47 |
SS |
2018-03-06 12:00 |
Okinawa |
|
A symbolic Zone-based reachability analysis for dense-timed pushdown automata with freezing clocks Shoji Yuen, Sho Hiraoka (Nagoya Univ.) SS2017-65 |
We present a reachability analysis by the zone-based symbolic discretization
for dense-timed pushdown automata with fre... [more] |
SS2017-65 pp.7-12 |
QIT (2nd) |
2017-11-17 10:00 |
Saitama |
Saitama University |
Limit on Quantum State Generation under Dissipation Kohei Kobayashi, Naoki Yamamoto (Keio Univ.) |
To realize quantum information technology, control for generating a target quantum state is highly necessary. However, i... [more] |
|
ET |
2016-03-05 16:15 |
Kagawa |
Kawaga Univ. (Saiwai-cho Campus) |
A Proposal for a Misconfiguration Detection Method based on Program Analysis Techniques for Network Construction Exercises for Beginners Yuichiro Tateiwa, Naohisa (NIT) ET2015-106 |
In this study, we propose a method that specifies regions (we call them fault regions) where misconfigurations concernin... [more] |
ET2015-106 pp.71-76 |
COMP |
2013-04-24 10:00 |
Hyogo |
Kobe University |
Answering Reachability Queries by Extending Pruned BFSs to Paths Yosuke Yano, Takuya Akiba, Yoichi Iwata (Univ. of Tokyo) COMP2013-1 |
The graph reachability is a fundamental problem, both theoretically and practically. However, it is still a challenging ... [more] |
COMP2013-1 pp.1-8 |
MSS |
2013-01-22 14:25 |
Osaka |
Osaka Int. Convention Center |
On Polynomial Time Checking on Reachability in Sound Extended Free-Choice Workflow Nets Daiki Kano, Shingo Yamaguchi (Yamaguchi Univ.) MSS2012-48 |
There are two aspects of a workflow: definition and instance.
In this paper, we tackle verification of correctness of w... [more] |
MSS2012-48 pp.17-21 |
MSS |
2013-01-22 14:50 |
Osaka |
Osaka Int. Convention Center |
On Analysis on Reachability to Unsafe Markings in Free Choice Workflow Nets Yuki Murakami, Ichiro Toyoshima, Shingo Yamaguchi (Yamaguchi Univ.) MSS2012-49 |
In the Free Choice Workflow net, the marking always reach to non-safety marking means that the workflow's instance can... [more] |
MSS2012-49 pp.23-26 |
CAS, MSS |
2011-11-18 11:15 |
Yamaguchi |
Univ. of Yamaguchi |
On Reachability Verification for Acyclic Well-Structured Work Shinji Hamano, Shingo Yamaguchi (Yamaguchi Univ.) CAS2011-78 MSS2011-47 |
Workflow nets are making great contributions for modeling and analysis of workflows.
In this paper, we tackle verificat... [more] |
CAS2011-78 MSS2011-47 pp.83-87 |
MSS, CAS |
2010-11-18 10:55 |
Osaka |
Kansai Univ. |
A Probability-based State Space Analysis of Petri Nets Eleazar Jimenez Serrano (Kyushu Univ.) CAS2010-66 CST2010-39 |
We present a partial exploration metaheuristic method of state spaces derived from Petri nets for the analysis of reacha... [more] |
CAS2010-66 CST2010-39 pp.7-12 |
DC |
2010-10-14 15:10 |
Tokyo |
Kikai-Shinko-Kaikan Bldg |
Accelerating State Reachability Analysis with a GPU Yoshimitsu Nakada, Tatsuhiro Tsuchiya, Tohru Kikuno (Osaka Univ.) DC2010-22 |
Reachability analysis is the process of exploring the state space of a system under verification. This step is fundament... [more] |
DC2010-22 pp.25-29 |
MSS |
2009-06-03 16:50 |
Osaka |
Setsunan University, Osaka Center |
[Invited Talk]
Probabilic Timed CEGAR Atsushi Morishita, Ryota Komagata, Satoshi Yamane (Kanazawa Univ.) CST2009-5 |
In this paper, we present an efficient verification method for probabilic timed automaton. This method based on predicat... [more] |
CST2009-5 pp.25-30 |
MSS |
2009-06-04 10:25 |
Osaka |
Setsunan University, Osaka Center |
On Reachability Analysis of Multi Agent Nets by Using Modular Petri Nets Kyota Horiguchi, Toshiyuki Miyamoto (Osaka Univ.) CST2009-6 |
Multi agent net is a formal model description language for multi agent systems. As a variant of Petri nets, modular Petr... [more] |
CST2009-6 pp.31-36 |
SS |
2009-03-02 17:00 |
Saga |
Saga University |
[Invited Talk]
Model Checking of Timed Automata Akio Nakata (Hiroshima City Univ.) SS2008-53 |
In this paper, we briefly describe model checking of timed automata, one of the verification techniques of real-time sys... [more] |
SS2008-53 pp.29-34 |
MSS |
2009-01-30 09:55 |
Kanagawa |
Kanagawa Industrial Promotion Center |
Modeling and Verification of Hybrid Systems using Boolean Differential Constraints Daisuke Ishii, Kazunori Ueda (Waseda Univ.), Hiroshi Hosobe (National Inst. of Info.) CST2008-53 |
We propose a bounded model checking method for reachability analysis of hybrid systems. In our method, a nonlinear hybri... [more] |
CST2008-53 pp.67-70 |
CAS, MSS |
2008-11-06 16:15 |
Osaka |
Osaka University |
Predicate Abstraction and Refinement of Parallel Behaviour of Hierarchical Timed Automata Shinichi Yamazaki, Satoshi Yamane, Masatoshi Yasui (Kanazawa Univ.) CAS2008-50 CST2008-28 |
In this paper, we propose the predicate abstraction and refinement verification method for the paralell hierarchical tim... [more] |
CAS2008-50 CST2008-28 pp.31-36 |
MSS |
2008-06-03 10:50 |
Aichi |
Nagoyo University, Noyori Conference Hall |
Reachability analysis method of probabilistic timed automaton based on predicate abstraction and its refinement Ryota Komagata, Atsushi Morishita, Satoshi Yamane (Kanazawa Univ.) CST2008-5 |
In this paper, we first define the Probabilic Timed Automaton. Next, we present an efficient verification method for Pro... [more] |
CST2008-5 pp.1-6 |