Forward analysis and model checking for trace bounded WSTS
详细信息 查看全文
- 作者：Pierre Chambarta ; Alain Finkelb ; Alain.Finkel@lsv.ens-cachan.fr" class="auth_mail" title="E-mail the corresponding author ; Sylvain Schmitzb
- 关键词：Complete WSTS ; Model checking ; Flattable system ; Bounded language ; Acceleration
- 刊名：Theoretical Computer Science
- 出版年：2016
- 出版时间：18 July 2016
- 年：2016
- 卷：637
- 期：Complete
- 页码：1-29
- 全文大小：1023 K
文摘
- •
The trace boundedness is decidable for complete deterministic WSTS.
- •
The downward-closure of the reachability set is computable for trace bounded complete deterministic WSTS.
- •
Action-based LTL model-checking is decidable for trace bounded complete deterministic WSTS.
- •
State-based LTL model-checking is undecidable for trace bounded complete deterministic WSTS.