Name
Abstract | ||
|---|---|---|
In this paper, we examine the subclass of RTL formulas considered in [14, 15] which we call path RTL. We propose a formal semantic extension of path RTL covering nonexistent event occurrences and show that all systems specified in path RTL can be reduced to systems which have infinitely many occurrences of all event types. We then show the undecidability of the path RTL satisfiability problem, give a PTIME algorithm for positive cycle detection, and give examples to show why refutation by positive cycles is incomplete for the path RTL satisfiability problem. Finally, we discussed a subclass of path RTL for which refutation by positive cycles is sound and complete in regard to the satisfiability problem. |
Year | DOI | Venue |
|---|---|---|
1994 | 10.1007/3-540-58555-9_121 | FME |
Keywords | Field | DocType |
positive cycles,satisfiability,formal semantics | Event type,Computer science,Boolean satisfiability problem,P,Cycle detection,Theoretical computer science | Conference |
ISBN | Citations | PageRank |
3-540-58555-9 | 11 | 0.60 |
References | Authors | |
10 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Farn Wang | 1 | 11 | 0.60 |
| Aloysius K. Mok | 2 | 662 | 86.52 |