2013/12/03 by Yong Wang, Wang, Yong
Computer Science · Mathematics · #Action (physics) #Algebra over a field #Axiom #Computer science #Correctness #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Mathematics #Operator (biology) #Process (computing) #Process calculus #Programming language #Pure mathematics #Rewriting #Semantic Web and Ontologies #Theoretical computer science #cs.LO
paper · pdf · doi:10.48550/arxiv.1312.0686
published in arXiv (Cornell University) (Cornell University) · 24 pages, 16 figures
openalex publication_date 2013/12/03 · arxiv created 2019/05/08 · arxiv updated 2019/05/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Using formal tools in computer science to describe games is an interesting problem. We give games, exactly two person games, an axiomatic foundation based on the process algebra ACP (Algebra of Communicating Process). A fresh operator called opponent's alternative composition operator (OA) is introduced into ACP to describe game trees and game strategies, called GameACP. And its sound and complete axiomatic system is naturally established. To model the outcomes of games (the co-action of the player and the opponent), correspondingly in GameACP, the execution of GameACP processes, another operator called playing operator (PO) is extended into GameACP. We also establish a sound and complete axiomatic system for PO. To overcome the new occurred non-determinacy introduced by GameACP, we extend truly concurrent process algebra APTC for games called GameAPTC. Finally, we give the correctness theorem between the outcomes of games and the deductions of GameACP and GameAPTC processes.