A deductive approach towards reasoning about algebraic transition systems
type: Item
instance of: scholarly article
title: A deductive approach towards reasoning about algebraic transition systems
zbMATH Open document ID: 1394.68248
DOI: 10.1155/2015/607013
author: Jun Fu
author: Jinzhao Wu
author: Hongyan Tan
published in: Mathematical Problems in Engineering
publication date: 2018-08-27T00:00:00Z
review text: Summary: 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.
Mathematics Subject Classification ID: 68Q85
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 6926770
Wikidata QID: Q59119538
describes a project that uses: TLAPS
describes a project that uses: STeP
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1155/2015/607013
OpenAlex ID: W2130420956
cites work: Model-based testing of reactive systems. Advanced lectures.
cites work: Formal verification of parallel programs
cites work: Non-linear loop invariant generation using Gröbner bases
cites work: Q3413659
cites work: Q5322945
cites work: A classification of symbolic transition systems
cites work: Verification of infinite-state dynamic systems using approximate quotient transition systems
cites work: Differential dynamic logic for hybrid systems
cites work: Q4539645
cites work: Q4525781
cites work: Temporal logic and state systems
cites work: Logics of specification languages
cites work: TLA + Proofs
cites work: Q5310200
cites work: The Complete Proof Theory of Hybrid Systems
cites work: Q4282674
cites work: Q5339289
cites work: The liberalized \(\delta\)-rule in free variable semantic tableaux
cites work: Cut-Elimination and Proof Schemata
cites work: Q4003735
cites work: Hybrid Systems: Computation and Control
cites work: Generating invariants for non-linear loops by linear algebraic methods
cites work: Property-directed incremental invariant generation
cites work: Q4391231
cites work: Symbolic techniques in satisfiability solving
cites work: Q4391232
description: scientific article; zbMATH DE number 6926770