Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2412.15799

Checking Timed Bisimilarity with Virtual Clocks

Alexander Lieb·Hendrik Göttmann·Lars Luthmann·Malte Lochau·Andy Schürr
View original source ↗Read source document ↗Export metadata ↓

Abstract

Timed automata are a widely used formalism for specifying the discrete-state/continuous-time behavior of time-critical reactive systems. For the fundamental verification problem of comparing two timed automata, it has been shown that timed trace equivalence is undecidable, while timed bisimulation is decidable. The corresponding decidability proof uses region graphs, a finite but space-consuming characterization of timed automata semantics. Most verification tools use zone graphs instead, a symbolic and, on average, more space-efficient representation of timed automata semantics. However, zone graphs provide correct results only for those verification tasks that are reducible to reachability problems, and are too imprecise for timed bisimilarity checking. To the best of our knowledge, there is currently no practical tool for automated timed bisimilarity checking. In this paper, we propose a new representation of timed automata semantics that extends zone graphs by so-called virtual clocks. Our zone-based construction is, on average, significantly smaller than the corresponding region graph representation. We also present experimental results obtained by applying our tool implementation to timed automata models, which are often used to evaluate timed automata analysis techniques.

Explore related subjects

cs.FL

Keep this discovery

BibTeXRIS

Alexander Lieb, Hendrik Göttmann, Lars Luthmann, Malte Lochau, Andy Schürr. 2026-08-31. Checking Timed Bisimilarity with Virtual Clocks. https://doi.org/10.46298/fi.15143

Cite the original work for its findings. Save a collection to share your selection of sources.

Discover connections

cs.FL subject

Connections use source metadata and explicit phrase matches, not verified experimental comparisons.

KEEP EXPLORING

Related papers

arXiv2026

CARVY-FL: Client Anticlustering for Robust Voting in Provably Secure Federated Learning

Federated learning (FL) enables collaborative training without directly sharing raw data, but remains vulnerable to malicious clients. Voting-based FL improves robustness by partitioning clients into groups, training one model per group, and aggregating predictions by plurality voting. However, under class-disjoint non-IID data, distribution-oblivious grouping can yield highly variable certified accuracy (CA). We propose CARVY-FL, which estimates client distribution types from one-epoch model updates and uses anticlustering to increase within-group distributional diversity. Under a fixed grouping, CARVY-FL retains the voting-based CA guarantee while increasing vote margins. Experiments on MNIST and Fashion-MNIST show higher CA than FLCert. Under BadNets with model replacement, CARVY-FL improves the AUC of 100-ASR by 11.1% and 14.9%, respectively.

cs.CR↗
arXiv2026

DART-FL: Burst-Aware Multitask Federated Learning under Dynamic Inference Demand at the Edge

Edge intelligence systems increasingly require model training and online inference to coexist on resource-constrained devices, while inference demand can vary substantially across tasks over time. This creates two coupled challenges: sufficient computation must be reserved for inference to maintain service-level objectives (SLOs), while the remaining training capacity should adapt to task-specific demand so that frequently requested tasks can improve earlier during training. We propose an SLO-aware, demand-driven multitask federated learning framework (DART-FL) that jointly adapts the inference-training resource split and task-level training emphasis. At each scheduling interval, DART-FL uses the inference backlog and profiled service capacity to determine the minimum resource allocation required for inference. The remaining training capacity is then distributed across tasks using a queue-aware DPP-inspired scheduler, and the resulting task allocations are mapped to dynamic loss weights. This allows tasks experiencing higher inference demand to receive greater training emphasis in earlier communication rounds. Clients train a shared backbone with task-specific heads, and the complete multitask model is aggregated through FedAvg. We evaluate DART-FL using Stanford Cars and Oxford Flowers 102 under both synthetic and real Alibaba trace-derived workloads. Results show that DART-FL dynamically adapts the inference-training resource split to time-varying inference demand and shifts the learning progress of high-demand tasks toward their burst periods, improving model accuracy when those tasks are frequently requested while maintaining comparable long-term multitask performance.

cs.LG↗
arXiv2026

SeaCausal-FL: Federated Fuzzy Causal Learning for Maritime IoT Fault Diagnosis and Counterfactual Reasoning

Reliable marine-engine fault diagnosis in maritime IoT is challenged by distributed data ownership, heterogeneous fault distributions, and continuously changing operating conditions. This paper proposes SeaCausal-FL, a federated fuzzy causal learning framework that combines a shared temporal diagnostic path with mechanism-conditioned causal reasoning. An interval type-2 fuzzy layer represents uncertain and overlapping operating mechanisms, while each mechanism is associated with a physics-constrained structural causal model. Before aggregation, locally learned mechanisms are aligned using operating context, causal structure, and conditional intervention-response signatures. Model parameters are then aggregated according to sample, class, mechanism, and mechanism-class evidence instead of client sample size alone. The learned structural equations further support interval counterfactual reasoning through abduction, action, and prediction. Experiments on a marine-engine fault dataset and a real-data-calibrated semi-synthetic causal benchmark show that SeaCausal-FL achieves an average F1 score of 87.07% across four client partitions, with AUROC and AUPRC of 98.98% and 94.81%, respectively. It also maintains strong performance under unseen loads and fault-type omission during training. On the causal benchmark, SeaCausal-FL reaches an Edge-F1 of approximately 0.58 and an Edge-AUPRC of 0.68, reduces coefficient RMSE to about 0.14, and provides favorable counterfactual estimation and intervention decisions.

cs.LG↗