Finite Uniform Bisimulations for Linear Systems with Finite Input Alphabets
Donglei Fan, Danielle C. Tarraf

TL;DR
This paper introduces finite uniform bisimulations for linear discrete-time systems with finite input sets, providing conditions for their existence and algorithms for their computation, supported by illustrative examples.
Contribution
It formulates a new notion of regular finite uniform bisimulation and derives conditions and algorithms for their computation in linear systems.
Findings
Sufficient conditions for the existence of finite uniform bisimulations.
Algorithms to compute finite uniform bisimulations.
Illustrative examples demonstrating the concepts.
Abstract
We consider a class of systems over finite alphabets, namely discrete-time systems with linear dynamics and a finite input alphabet. We formulate a notion of finite uniform bisimulation, and motivate and propose a notion of regular finite uniform bisimulation. We derive sufficient conditions for the existence of finite uniform bisimulations, and propose and analyze algorithms to compute finite uniform bisimulations when the sufficient conditions are satisfied. We investigate the necessary conditions, and conclude with a set of illustrative examples.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Petri Nets in System Modeling · Real-Time Systems Scheduling
