Home // COMPUTATION TOOLS 2016, The Seventh International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking // View article

Logical Characterization and Complexity of Weighted Branching Preorders and Distances

Authors:
Louise Foshammer
Kim Guldstrand Larsen
Radu Mardare
Bingtian Xue

Keywords: Weighted transition systems; Weighted computational tree logic; Characterization; Weighted branching bisimulation

Abstract:
We investigate branching bisimulation for weighted transition systems. It is known that branching bisimulation is characterized by computational tree logic without the next operator in the non-deterministic case. We demonstrate that the weighted version of this logic characterizes a weighted version of branching bisimulation, for which the decidability is NP-complete. This leads us to investigating two fragments of this logic allowing only upper bounds and either existential or universal quantification. The resulting existential and universal simulation relations are decidable in polynomial time. We consider distance-based analogues of weighted branching bisimulation and existential simulation and characterize these using fragments of the aforementioned logic.

Pages: 12 to 18

Copyright: Copyright (c) IARIA, 2016

Publication date: March 20, 2016

Published in: conference

ISSN: 2308-4170

ISBN: 978-1-61208-466-4

Location: Rome, Italy

Dates: from March 20, 2016 to March 24, 2016