A Deductive Approach towards Reasoning about Algebraic Transition Systems

Jun Fu, Jinzhao Wu and Hongyan Tan

Mathematical Problems in Engineering, 2015, vol. 2015, 1-12

Abstract:

Algebraic transition systems are extended from labeled transition systems by allowing transitions labeled by algebraic equations for modeling more complex systems in detail. We present a deductive approach for specifying and verifying algebraic transition systems. We modify the standard dynamic logic by introducing algebraic equations into modalities. Algebraic transition systems are embedded in modalities of logic formulas which specify properties of algebraic transition systems. The semantics of modalities and formulas is defined with solutions of algebraic equations. A proof system for this logic is constructed to verify properties of algebraic transition systems. The proof system combines with inference rules decision procedures on the theory of polynomial ideals to reduce a proof-search problem to an algebraic computation problem. The proof system proves to be sound but inherently incomplete. Finally, a typical example illustrates that reasoning about algebraic transition systems with our approach is feasible.

Date: 2015
References: Add references at CitEc
Citations:

Downloads: (external link)
http://downloads.hindawi.com/journals/MPE/2015/607013.pdf (application/pdf)
http://downloads.hindawi.com/journals/MPE/2015/607013.xml (text/xml)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:hin:jnlmpe:607013

DOI: 10.1155/2015/607013

Access Statistics for this article

More articles in Mathematical Problems in Engineering from Hindawi
Bibliographic data for series maintained by Mohamed Abdelhakeem ().