dc.contributor.author | URSU, A. | |
dc.contributor.author | GRUITA, G. | |
dc.contributor.author | ZAPOROJAN, S. | |
dc.date.accessioned | 2020-12-17T15:44:15Z | |
dc.date.available | 2020-12-17T15:44:15Z | |
dc.date.issued | 1997 | |
dc.identifier.citation | URSU, A., GRUITA, G., ZAPOROJAN, S. Design of the Sequential System Automata using Temporal Equivalence Classes. In: Computer Science Journal of Moldova. 1997, Vol 5, nr. 2(14), pp.330-352. ISSN 1561-4042. | en_US |
dc.identifier.uri | http://repository.utm.md/handle/5014/12187 | |
dc.description.abstract | A design method of sequential system automata using temporal logic specifications is proposed in this paper. The method is based on well-known Z.Manna and P.Wolper temporal logic satisfiability analysis procedure and is extended to include past time temporal operators. A new specification method which uses temporal equivalence classes is proposed to specify the behaviour of large digital circuits.The impact of the composition and decomposition operations of the temporal equivalence classes on the final automata has been studied. A case study is carried out which deals with the design of the synchronous bus arbiter circuit element. The SMV tool has been used to verify the temporal properties of the obtained automata. Key words: Temporal Logic, Temporal Equivalence Classes, Temporal Logic Specifications, Sequential Systems, Automata. | en_US |
dc.language.iso | en | en_US |
dc.publisher | Institute of Mathematics and Computer Science | en_US |
dc.rights | Attribution-NonCommercial-NoDerivs 3.0 United States | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/3.0/us/ | * |
dc.subject | design | en_US |
dc.subject | method | en_US |
dc.subject | past time temporal operators | en_US |
dc.subject | large digital circuits | en_US |
dc.title | Design of the Sequential System Automata using Temporal Equivalence Classes | en_US |
dc.type | Article | en_US |
The following license files are associated with this item: