A linear algorithm to solve fixed-point equations on transition systems

作者: André Arnold , Paul Crubille

DOI: 10.1016/0020-0190(88)90029-4

关键词:

摘要: Abstract This paper gives an algorithm to compute the least fixed-point of a system equations over transition system. has time complexity linear in size system, thus improving known algorithms which are quadratic.

参考文章(7)
Joseph Sifakis, A unified approach for studying the properties of transition systems Theoretical Computer Science. ,vol. 18, pp. 227- 258 ,(1982) , 10.1016/0304-3975(82)90067-6
Robert M. Keller, Formal verification of parallel programs Communications of The ACM. ,vol. 19, pp. 371- 384 ,(1976) , 10.1145/360248.360251
Dexter Kozen, Results on the propositional μ-calculus Theoretical Computer Science. ,vol. 27, pp. 333- 354 ,(1983) , 10.1016/0304-3975(82)90125-6
E. M. Clarke, E. A. Emerson, A. P. Sistla, Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach symposium on principles of programming languages. pp. 117- 126 ,(1983) , 10.1145/567067.567080
Anne Dicky, An algebraic and algorithmic method for analysing transition systems Theoretical Computer Science. ,vol. 46, pp. 285- 303 ,(1986) , 10.1016/0304-3975(86)90034-4
E. M. Clarke, E. A. Emerson, A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications ACM Transactions on Programming Languages and Systems. ,vol. 8, pp. 244- 263 ,(1986) , 10.1145/5397.5399
Robert Tarjan, Depth-First Search and Linear Graph Algorithms SIAM Journal on Computing. ,vol. 1, pp. 146- 160 ,(1972) , 10.1137/0201010