IRTUM – Institutional Repository of the Technical University of Moldova

Design of the Sequential System Automata using Temporal Equivalence Classes

Show simple item record

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


Files in this item

The following license files are associated with this item:

This item appears in the following Collection(s)

Show simple item record

Attribution-NonCommercial-NoDerivs 3.0 United States Except where otherwise noted, this item's license is described as Attribution-NonCommercial-NoDerivs 3.0 United States

Search DSpace


Browse

My Account