A Complete Approximation Theory for Weighted Transition Systems
Authors
Christoffersen, Peter ; Pedersen, Mathias Ruggaard ; Hansen, Mikkel
Term
4. term
Education
Publication year
2015
Submitted on
2015-06-01
Pages
32
Abstract
I mange modeller af dynamiske systemer er tilstande forbundet af overgange med vægte, der beskriver kvantitativ information. De præcise vægte er ikke altid kendte, så vi har brug for at kunne ræsonnere under usikkerhed. Vi foreslår generaliserede vægtede transitionssystemer (GTS), som udvider klassiske vægtede transitionssystemer ved at erstatte hver præcis vægt med et interval af ikke‑negative reelle tal. Disse intervaller angiver nedre og øvre grænser for, hvad en overgang kan veje. Vi udvikler en modallogik til GTS, der tilpasser operatorer fra probabilistiske logikker til en vægtet kontekst. Logikken gør det muligt at udtrykke udsagn som: der findes en overgang til en tilstand med en given egenskab, hvis vægt er mindst en given tærskel, eller højst en given tærskel. Dermed får vi et formelt sprog til approksimativ ræsonnering over intervalvægte. Vi viser, at logikken opfylder Hennessy–Milner‑egenskaben: den skelner ikke mellem systemer, der er adfærdsmæssigt ækvivalente i kraft af en passende bisimulation for GTS. Vores hovedbidrag er en aksiomatisering, der er sund og svagt fuldstændig: alle udledelige formler er sande i alle GTS‑modeller, og alle universelt gyldige formler kan udledes. Fuldstændigheden bevises ved en standardteknik i modal og Markoviansk logik via konstruktion af en kanonisk model.
In many models of dynamic systems, states are connected by transitions that carry weights, capturing quantitative information. Exact weights are not always known, so we need ways to reason under uncertainty. We propose Generalized Weighted Transition Systems (GTS), which extend standard weighted transition systems by replacing each exact weight with an interval of non‑negative real numbers. These intervals capture lower and upper bounds on what a transition may weigh. We design a modal logic for GTS that adapts operators from probabilistic logics to a weighted setting. The logic lets us express statements such as: there exists a transition to a state with a given property whose weight is at least a threshold, or at most a threshold. This provides a formal language for approximate reasoning over interval weights. We show that the logic satisfies the Hennessy–Milner property: it does not distinguish systems that are behaviorally equivalent according to an appropriate bisimulation for GTS. Our main technical result is an axiomatization that is sound and weakly complete: all derivable formulas are true in every GTS model, and every universally valid formula can be derived. The completeness proof follows a standard technique in modal and Markovian logics by constructing a canonical model.
[This abstract was generated with the help of AI]
Keywords
Documents