2026-08-17T03:18:41Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9693 2024-03-06T10:44:50Z ddc:004 open_access

Finite Bisimulations for Dynamical Systems with Overlapping Trajectories Bérard, Béatrice Bouyer, Patricia Jugé, Vincent Reachability properties dynamical systems o-minimal structures intersecting trajectories finite bisimulations Having a finite bisimulation is a good feature for a dynamical system, since it can lead to the decidability of the verification of reachability properties. We investigate a new class of o-minimal dynamical systems with very general flows, where the classical restrictions on trajectory intersections are partly lifted. We identify conditions, that we call Finite and Uniform Crossing: When Finite Crossing holds, the time-abstract bisimulation is computable and, under the stronger Uniform Crossing assumption, this bisimulation is finite and definable. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Béatrice Bérard and Patricia Bouyer and Vincent Jugé 2018 Is Part Of LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2018.26 urn:nbn:de:0030-drops-96932 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.26 eng https://creativecommons.org/licenses/by/3.0/legalcode