[36]
Towards Model-Driven Heat PumpControl in a Multi-Story BuildingbyI.R. HasratK.H. AndersenP.G. JensenR.L. JensenK.G. LarsenJ. SrbaJournal of Building Performance Simulationpages 1--21Taylor and Francis2025 To appear.PDFTaylor and FrancisBibTexAbstractDomestic heating systems exhibit significant energy flexibility when integrated with heat pumps andhot-water buffer tanks,
especially with fluctuating day-ahead energy prices. However, optimizingthese systems in large buildings with shared resources
poses crucial challenges. While most existingmethods target single-room or single-family houses,this study delves into complexities
within a three-story building housing six apartments. The building's heating system comprises a hot water buffertank, mixing
loop, floor heaters, and a Ground Source Heat Pump (GSHP) controlled by a weather-compensated control strategy (WCS). Our
approach aims to tackle challenges like integrating realsensor data, scalability, varying weather effects, and diverse resident
heat use preferences. We employCTSM software to identify thermal behaviour and use reinforcement learning to design an intelligentUppaal
Stratego controller. Our results reveal a 43% reduction in energy costs while maintainingcomfort levels compared to WCS. The
temporal validity of estimated thermal models is also analyzed.
[35]
Measurement-Noise Filtering for Automatic Discovery of Flow Splitting Ratios in ISP NetworksbyM.K. SchouI. PoeseJ. SrbaFormal Aspects of Computingpages 1--18Elsevier Science2024PDFElsevier ScienceEEBibTexAbstractNetwork telemetry and analytics is essential for providing highly dependable services in modern computer networks. In particular,
network flow analytics for ISP networks allows operators to inspect and reason about traffic patterns in their networks in
order to react to anomalies. High performance network analytics systems are designed with scalability in mind, and can consequently
only observe partial information about the network traffic. Still, they need to provide a holistic view of the traffic, including
the distribution of different traffic flows on each link. It is impractical to monitor such fine-grained telemetry, and in
large, heterogeneous networks it is often too complex and error-prone, if not impossible, to access and maintain all technical
specifications and router-specific configurations needed to determine e.g. the load balancing weights used when traffic is
split onto multiple paths. The ratios by which flows are split on the possible paths must be derived indirectly from the measured
flow demands and link utilizations. Motivated by a case study provided by a major European ISP, we suggest an efficient method
to estimate the flow splitting ratios. Our approach, based on quadratic linear programming, is scalable and achieves robustness
to the measurement noise found in a typical network analytics deployment by filtering out certain constraints in the linear
program. Finally, we implement an automated tool for estimating the flow splitting ratios and document its applicability on
real data from the ISP.
[34]
Optimal Control Strategies for Stormwater Detention PondsbyM.A. GoordenK.G. LarsenJ.E. NielsenT.D. NielsenW. QianM.R. RasmussenJ. SrbaG. ZhaoNonlinear Analysis: Hybrid Systems
volume 53ofpages 1--15Elsevier Science2024PDFElsevier ScienceEEBibTexAbstractStormwater detention ponds are essential stormwater management solutions that regulate the urban catchment discharge towards
streams. Their purposes are to reduce the hydraulic load to avoid stream erosion, as well as to minimize the degradation of
the natural waterbody by direct discharge of pollutants. Currently, static controllers are widely implemented for detention
pond outflow regulation in engineering practice, i.e., the outflow discharge is capped at a fixed value. Such a passive discharge
setting fails to exploit the full potential of the overall water system, hence further improvements are needed. We apply formal
methods to synthesize (i.e., derive automatically) optimal active controllers. We model the stormwater detention pond, including
the urban catchment area and the rain forecasts with its uncertainty, as hybrid Markov decision processes. Subsequently, we
use the tool Uppaal Stratego to synthesize using Q-learning a control strategy maximizing the retention time for pollutant
sedimentation (optimality) while also minimizing the duration of emergency overflow in the detention pond (safety). These
strategies are synthesized for both an off-line and on-line settings. Simulation results for an existing pond show that Uppaal
Stratego can learn optimal strategies that significantly reduce emergency overflows. For off-line controllers, a scenario
with low rain periods shows a 26% improvement of pollutant sedimentation with respect to static control, and a scenario with
high rain periods shows a reduction of overflow probability of 10%-19% for static control to lower than 5%, while pollutant
sedimentation has only declined by 7% compared to static-control. For on-line controllers, one scenario with heavy rain shows
a 95% overflow duration reduction and a 29% pollutant sedimentation improvement compared to static control.
[33]
Kaki: Efficient Concurrent Update Synthesis for SDNbyN.S. JohansenL.B. KaerA.L. MadsenK.O. NielsenJ. SrbaR.G. TollundFormal Aspects of Computing
volume 35(3)ofpages 1--22ACM2023PDFACMEEBibTexAbstractModern computer networks based on the software-defined networking (SDN) paradigm are becoming increasingly complex and often
require frequent configuration changes in order to react to traffic fluctuations. It is essential that forwarding policies
are preserved not only before and after the configuration update but also at any moment during the inherently distributed
execution of such an update. We present Kaki, a Petri game based tool for automatic synthesis of switch batches which can
be updated in parallel without violating a given (regular) forwarding policy like waypointing or service chaining. Kaki guarantees
to find the minimum number of concurrent batches and supports both splittable and nonsplittable flow forwarding. In order
to achieve optimal performance, we introduce two novel optimisation techniques based on static analysis: decomposition into
independent subproblems and identification of switches that can be collectively updated in the same batch. These techniques
considerably improve the performance of our tool Kaki, relying on TAPAAL's verification engine for Petri games as its backend.
Experiments on a large benchmark of real networks from the Internet Topology Zoo database demonstrate that Kaki outperforms
the state-of-the-art tools Netstack and FLIP. Kaki computes concurrent update synthesis significantly faster than Netstack
and compared to FLIP, it provides shorter (and provably optimal) concurrent update sequences at similar runtimes.
[32]
A Toolchain for Domestic Heat-Pump Control Using UPPAAL STRATEGObyI.R. HasratP.G. JensenK.G. LarsenJ. SrbaScience of Computer Programming
volume 230ofpages 1--20Elsevier Science2023PDFElsevier ScienceEEBibTexAbstractHeatpump-based floor-heating systems for domestic heating offer flexibility in energy consumption patterns, which can be utilized
for reducing heating costs-in particular whenconsidering hour-based electricity prices. Such flexibility is hard to exploit
via classicalModel Predictive Control (MPC), and in addition, MPC requires a priori calibration (i.e.,model identification)
which is often costly and becomes outdated as the dynamics anduse of a building change. We solve these shortcomings by combining
recent advancementsin stochastic model identification and automatic (near-)optimal controller synthesis. Ourmethod suggests
an adaptive model-identification using the tool CTSM-R, and an efficientcontrol synthesis based on Q-learning for Euclidean
Markov Decision Processes via UppaalStratego. This paper investigates three potential control strategy perspectives (i.e.,
fixed-target, target-band, and setbacks) to achieve energy efficiency in the heating system. Toexamine the performance of
the suggested approaches, we demonstrate our method on anexperimental Danish family-house from the OpSys project. The results
show that a fixed-target strategy offers up to a 39% reduction in heating cost while retaining comparablecomfort to a standard
bang-bang controller. Even better, target-band and setbacks strategiesgain up to 46-49% energy cost savings. Furthermore,
we show the flexibility of our methodby computing the Pareto-frontier that visualizes the cost/comfort tradeoff. Additionally,we
discuss the applicability of Stratego for an old-fashioned binary-mode heat-pumpsystem and report significant cost savings
(33%) as compared to the bang-bang controller.Moreover, we also present the performance analysis of Stratego against an industry-standard
control strategy.
[31]
AllSynth: A BDD-Based Approach for Network Update SynthesisbyK.G. LarsenA. MariegaardS. SchmidJ. SrbaScience of Computer Programming
volume 230ofpages 1--19Elsevier Science2023PDFElsevier ScienceEEBibTexAbstractThe increasingly stringent dependability requirements on communication networks as well as the need to render these networks
more adaptive to improve performance, demand for more automated approaches to operate networks. We present AllSynth, a symbolic
synthesis tool for updating communication networks in a provably correct and efficient manner. AllSynth automatically synthesizes
network update schedules which transiently ensure a wide range of policy properties expressed using linear temporal logic
(LTL). In particular, in contrast to existing approaches, AllSynth symbolically computes and compactly represents all feasible
and cost-optimal solutions. At its heart, AllSynth relies on a novel parameterized use of binary decision diagrams (BDDs)
which greatly improves performance. Indeed, AllSynth not only provides formal correctness guarantees and outperforms existing
state-of-the-art tools in terms of generality, but also in terms of runtime as documented by experiments on a benchmark of
real-world network topologies.
[30]
Determine Stormwater Pond Geometrics and Hydraulics Using Remote Sensing Technologies: A Comparison between Airborne-LiDAR
and UAV-Photogrammetry Field Validation against RTK-GNSSbyG. ZhaoM.R. RasmussenK.G. LarsenJ. SrbaT.D. NielsenM. GoordenW. QianJ.E. NielsenJournal of Hydroinformatics
volume 254ofpages 1256--1275IWA Publishing2023PDFIWA PublishingEEBibTexAbstractFlow-regulated stormwater ponds providing safe outflow discharges prevail as the primary stormwater management tool for stream
protections. Detailed pond geometries are essential metrics in pond monitoring technologies, which convert the point-based
water level measurements to areal/volumetric ponding water estimations. Unlike labour-intensive surveys (e.g., RTK-GNSS or
total stations), UAV-photogrammetry and airborne-LiDAR have been advocated as cost-effective alternatives to acquire high-quality
datasets. In this paper, we compare the use of these two approaches for stormwater pond surveys. With reference to RTK-GNSS
in-situ observations, we identify their geometric and hydraulic discrepancies based on six stormwater ponds from three aspects:
(i) DEMs, (ii) stage-curves and (iii) outflow discharges. Three main findings are outlined: (i) for wet ponds where moisture
environments are dominant, UAV-photogrammetry outperforms (infrared) airborne-LiDAR, where airborne-LiDAR yields 0.15-0.54
NSEoutflow, which is unacceptable; (ii) for dry ponds, UAV-photogrammetry obtains 0.88-0.89 NSEoutflow as poor vegetation
penetrations; two correction methods (i.e., grass removal and shifted stage-curves) are proposed, indicating good alignment
to RTK-GNSS observations and (iii) UAV-photogrammetry delivers <0.1 m resolution in outlining break-line features for stormwater
pond structures. With significant economic advantages, the multi-UAV collaborative photogrammetry would address the shortcomings
of a single UAV and thus pave the way for large urban catchment/watershed survey applications.
[29]
Methods for Efficient Unfolding of Colored Petri NetsbyA. BilgramP.G. JensenT. PedersenJ. SrbaP.H. TaankvistFundamenta Informaticae
volume 1893--4ofpages 297-320IOS Press2023PDFIOS PressEEBibTexAbstractColored Petri nets offer a compact and user friendly representation of the traditional P/T nets and colored nets with finite
color ranges can be unfolded into the underlying P/T nets, however, at the expense of an exponential explosion in size. We
present two novel techniques based on static analysis in order to reduce the size of unfolded colored nets. The first method
identifies colors that behave equivalently and groups them into equivalence classes, potentially reducing the number of used
colors. The second method overapproximates the sets of colors that can appear in places and excludes colors that can never
be present in a given place. Both methods are complementary and the combined approach allows us to significantly reduce the
size of multiple colored Petri nets from the Model Checking Contest benchmark. We compare the performance of our unfolder
with state-of-the-art techniques implemented in the tools MCC, Spike and ITS-Tools, and while our approach is competitive
w.r.t. unfolding time, it also outperforms the existing approaches both in the size of unfolded nets as well as in the number
of answered model checking queries from the 2021 Model Checking Contest.
[28]
Automata-Theoretic Approach to Verification of MPLS Networks under Link FailuresbyI. van DuijnP.G. JensenJ.S. JensenT.B. KrøghJ.S. MadsenS. SchmidJ. SrbaM.T. ThorgersenIEEE/ACM Transactions on Networking
volume 302ofpages 766--781IEEE2022PDFIEEEEEBibTexAbstractFuture communication networks are expected to be highly automated, disburdening human operators of their most complex tasks.
While the first powerful and automated network analysis tools are emerging, existing tools provide only limited and inefficient
support of reasoning about failure scenarios. We present P-REX, a fast what-if analysis tool, that allows us to test important
reachability and policy-compliance properties even under an arbitrary number of failures and in polynomial-time, i.e., without
enumerating all failure scenarios (the usual approach today, if supported at all). P-REX targets networks based on Multiprotocol
Label Switching (MPLS) and its Segment Routing (SR) extension which feature fast rerouting mechanisms with label stacks. In
particular, P-REX allows to reason about recursive backup tunnels, by supporting potentially infinite state spaces. As P-REX
directly operates on the actual dataplane configuration, i.e., forwarding tables, it is well-suited for debugging. Our tool
comes with an expressive query language based on regular expressions. We also report on an industrial case study and demonstrate
that our tool can perform what-if reachability analyses on average in about 5 seconds for a 24-router network with over 250,000
MPLS forwarding rules. This is a significant improvement to an earlier prototype of our tool presented in the conference version
of our paper where the verification took on average about 1 hour.
[27]
Extended Abstract Dependency GraphsbyS. EnevoldsenK.G. LarsenJ. SrbaInternational Journal on Software Tools for Technology Transfer (STTT)
volume 24ofpages 49--65Springer-Verlag2022PDFSpringer-VerlagEEBibTexAbstractDependency graphs, invented by Liu and Smolka in 1998, are oriented graphs with hyperedges that represent dependencies among
the values of the vertices. Numerous model checking problems are reducible to a computation of the minimum fixed-point vertex
assignment. Recent works successfully extended the assignments in dependency graphs from the Boolean domain into more general
domains in order to speed up the fixed-point computation or to apply the formalism to a more general setting of, for example,
weighted logics. All these extensions require separate correctness proofs of the fixed-point algorithm as well as a one-purpose
implementation. We suggest the notion of extended abstract dependency graphs where the vertex assignment is defined over an
abstract algebraic structure of Noetherian partial orders with the least element, and where we allow both monotonic and non-monotonic
functions. We show that existing approaches are concrete instances of our general framework and provide an open-source C++
library that implements the abstract algorithm. We demonstrate that the performance of our generic implementation is comparable
to, and sometimes even outperforms, dedicated special-purpose algorithms presented in the literature.
[26]
Stubborn Set Reduction for Two-Player Reachability GamesbyF.M. BønnelandP.G. JensenK.G. LarsenM. MunizJ. SrbaLogical Methods in Computer Science
volume 171ofpages 1--26Creative Commons2021PDFCreative CommonsEEBibTexAbstractPartial order reductions have been successfully applied to model checking of concurrent systems and practical applications
of the technique show nontrivial reduction in the size of the explored state space. We present a theory of partial order reduction
based on stubborn sets in the game-theoretical setting of 2-player games with reachability objectives. Our stubborn reduction
allows us to prune the interleaving behaviour of both players in the game, and we formally prove its correctness on the class
of games played on general labelled transition systems. We then instantiate the framework to the class of weighted Petri net
games with inhibitor arcs and provide its efficient implementation in the model checker TAPAAL. Finally, we evaluate our stubborn
reduction on several case studies and demonstrate its efficiency.
[25]
Dependency Graphs with Applications to VerificationbyS. EnevoldsenK.G. LarsenA. MariegaardJ. SrbaInternational Journal on Software Tools for Technology Transfer (STTT)
volume 22ofpages 635--654Springer-Verlag2020PDFSpringer-VerlagEEBibTexAbstractDependency graphs, as introduced more than 20 years ago by Liu and Smolka, are oriented graphs with hyperedges that connect
nodes with sets of target nodes in order to represent causal dependencies in the graph. Numerous verification problems can
be reduced into the problem of computing a minimum or maximum fixed-point assignment on dependency graphs. In the original
definition, assignments link each node with a Boolean value, however, in the recent work the assignment domains have been
extended to more general setting, even including infinite domains. In this survey paper, we present an overview of the recent
results on extensions of dependency graphs in order to deal with verification of quantitative, probabilistic, parameterized
and timed systems.
[24]
Model Checking and Synthesis for Branching Multi-Weighted LogicsbyJ.S. JensenI. KaufmannK.G. LarsenS.M. NielsenJ. SrbaJournal of Logical and Algebraic Methods in Programming
volume 1051ofpages 28--46Elsevier Science2019PDFElsevier ScienceEEBibTexAbstractWe investigate the open synthesis problem in a quantitative game theoretic setting where the system model is annotated with
multiple nonnegative weights representing quantitative resources such as energy, discrete time or cost. We consider system
specifications expressed in the branching time logic CTL extended with bounds on resources. As our first contribution, we
show that the model checking problem for the full logic is undecidable with already three weights. By restricting the bounds
to constant upper or lower-bounds on the individual weights, we demonstrate that the problem becomes decidable and that the
model checking problem is PSPACE-complete. As a second contribution, we show that by imposing upper-bounds on the temporal
operators and assuming that the cost converges over infinite runs, the synthesis problem is also decidable. Finally, we provide
an on-the-fly algorithm for the synthesis problem on an unrestricted model for a reachability fragment of the logic and we
prove EXPTIME-completeness of the synthesis problem.
[23]
Stubborn Versus Structural Reductions for Petri NetsbyF. BønnelandJ. DyhrP.G. JensenM. JohannsenJ. SrbaJournal of Logical and Algebraic Methods in Programming
volume 1021ofpages 46--63Elsevier Science2019PDFElsevier ScienceEEBibTexAbstractPartial order and structural reduction techniques are some of the most beneficial methods for state space reduction in reachability
analysis of Petri nets. This is among others documented by the fact that these techniques are used by the leading tools in
the annual Model Checking Contest (MCC) of Petri net tools. We suggest improved versions of a partial order reduction based
on stubborn sets and of a structural reduction with additional new reduction rules, and we extend both methods for the application
on Petri nets with weighted arcs and weighted inhibitor arcs. All algorithms are implemented in the open-source verification
tool TAPAAL and evaluated on a large benchmark of Petri net models from MCC'17, including a comparison with the tool LoLA
(the last year winner of the competition). The experiments document that both methods provide significant state space reductions
and, even more importantly, that their combination is indeed beneficial as a further nontrivial state space reduction can
be achieved.
[22]
MCC'2017 - The Seventh Model Checking ContestbyF. KordonH. GaravelL.-M. HillahE. Paviot-AdetL. JezequelF. Hulin-HubardE.G. AmparoreM. BeccutiB. BerthomieuH. EvrardP.G. JensenD. Le BotlanT. LiebkeJ. MeijerJ. SrbaY. Thierry-MiegJ. van de PolK. WolfT. Petri Nets and Other Models of Concurrency
volume 13ofpages 181--209Springer-Verlag2018PDFSpringer-VerlagEEBibTexAbstractCreated in 2011, the Model Checking Contest (MCC) is an annualcompetition dedicated to provide a fair evaluation of software
tools thatverify concurrent systems using state-space exploration techniques andmodel checking. This article presents the
principles and results of the2017 edition of the MCC, which took place along with the Petri Net andACSD joint conferences
in Zaragoza, Spain.
[21]
A Distributed Fixed-Point Algorithm for Extended Dependency GraphsbyA.E. DalsgaardS. EnevoldsenP. FoghL.S. JensenP.G. JensenT.S. JepsenI. KaufmannK.G. LarsenS.M. NielsenM.Chr. OlesenS. PastvaJ. SrbaFundamenta Informaticae
volume 1614ofpages 351--381IOS Press2018PDFIOS PressEEBibTexAbstractEquivalence and model checking problems can be encoded into computing fixed points on dependency graphs. Dependency graphs
represent causal dependencies among the nodes of the graph by means of hyper-edges. We suggest to extend the model of dependency
graphs with so-called negation edges in order to increase their applicability. The graphs (as well as the verification problems)
suffer from the state space explosion problem. To combat this issue, we design an on-the-fly algorithm for efficiently computing
fixed points on extended dependency graphs. Our algorithm supplements previous approaches with the possibility to back-propagate,
in certain scenarios, the domain value 0, in addition to the standard back-propagation of the value 1. Finally, we design
a distributed version of the algorithm, implement it in our open-source tool TAPAAL, and demonstrate the efficiency of our
general approach on the benchmark of Petri net models and CTL queries from the annual Model Checking Contest.
[20]
Discrete and Continuous Strategies for Timed-Arc Petri Net GamesbyP.G. JensenK.G. LarsenJ. SrbaInternational Journal on Software Tools for Technology Transfer (STTT)
volume 205ofpages 529--546Springer-Verlag2018PDFSpringer-VerlagEEBibTexAbstractAutomatic strategy synthesis for a given control objective can be used to generate correct-by-construction controllers of
real-time reactive systems. The existing symbolic approach for continuous timed games is a computationally hard task and current
tools like UPPAAL TiGa often scale poorly with the model complexity. We suggest an explicit approach for strategy synthesis
in the discrete-time setting and show that even for systems with closed guards, the existence of a safety discrete-time strategy
does not imply the existence of a safety continuous-time strategy and vice versa. Nevertheless, we prove that the answers
to the existence of discrete-time and continuous-time safety strategies coincide on a practically motivated subclass of urgent
controllers that either react immediately after receiving an environmental input or wait with the decision until a next event
is triggered by the environment. We then develop an on-the-fly synthesis algorithm for discrete timed-arc Petri net games.
The algorithm is implemented in our tool TAPAAL and based on the experimental evidence, we discuss the advantages of our approach
compared to the symbolic continuous-time techniques.
[19]
TAPAAL and Reachability Analysis of P/T NetsbyJ.F. JensenT. NielsenL.K. OestergaardJ. SrbaLNCS Transactions on Petri Nets and Other Models of Concurrency (ToPNoC)
volume 9930ofpages 307--318Springer-Verlag2016PDFSpringer-VerlagEEBibTexAbstractWe discuss selected model checking techniques used in the tool TAPAAL for the reachability analysis of weighted Petri nets
with inhibitor arcs. We focus on techniques that had the most significant effect at the 2015 Model Checking Contest (MCC).
While the techniques are mostly well known, our contribution lies in their adaptation to the MCC reachability queries, their
efficient implementation and the evaluation of their performance on a large variety of nets from MCC'15.
[18]
Efficient Model Checking of Weighted CTL with Upper-Bound ConstraintsbyJ.F. JensenK.G. LarsenJ. SrbaL.K. OestergaardInternational Journal on Software Tools for Technology Transfer (STTT)
volume 184ofpages 409--426Springer-Verlag2016PDFSpringer-VerlagEEBibTexAbstractWe present a symbolic extension of dependency graphs by Liuand Smolka in order to model-check weighted Kripke structures againstthe
logic CTL with upper-bound weight constraints. Our extension introducesa new type of edges into dependency graphs and lifts
the computation offixed-points from boolean domain to nonnegative integers in order to copewith the weights. We present both
global and local algorithms for thefixed-point computation on symbolic dependency graphs and argue for theadvantages of our
approach compared to the direct encoding of the modelchecking problem into dependency graphs. We implement all algorithmsin
a publicly available tool prototype and evaluate them on severalexperiments. The principal conclusion is that our local algorithm
isthe most efficient one with an order of magnitude improvement formodel checking problems with a high number of `witnesses'.
[17]
Soundness of Timed-Arc Workflow Nets in Discrete and Continuous-Time SemanticsbyJ.A. MateoJ. SrbaM.G. SørensenFundamenta Informaticae
volume 1401ofpages 89--121IOS Press2015PDFIOS PressEEBibTexAbstractAnalysis of workflow processes with quantitative aspectslike timing is of interest in numerous time-critical applications.
We suggest a workflow model based on timed-arc Petri nets and studythe foundational problems of soundness and strong (time-bounded)
soundness.We first consider the discrete-time semantics (integer delays)and explore the decidability of the soundness problemsand
show, among others, that soundness is decidable for monotonic workflow nets while reachability is undecidable.For general
timed-arc workflow nets soundness andstrong soundness become undecidable, though we can design efficientverification algorithms
for the subclass of bounded nets. We also discuss the soundness problem in the continuous-timesemantics (real-number delays)
and show that for nets withnonstrict guards (where the reachability question coincides for bothsemantics) the soundness checking
problem does not in generalfollow the approach for the discrete semantics and different zone-basedtechniques are needed for
introducing its decidability in the bounded case.Finally, we demonstrate the usability of our theory onthe case studies of
a Brake System Control Unit used in aircraft certification, the MPEG2 encoding algorithm, and a blood transfusion workflow.The
implementation of the algorithms is freely available as a part of the model checker TAPAAL (www.tapaal.net).
[16]
Refinement Checking on Parametric Modal Transition SystemsbyN. BenesJ. KretinskyK.G. LarsenM.H. MøllerS. SickertJ. SrbaActa Informatica
volume 522--3ofpages 269--297Springer-Verlag2015PDFSpringer-VerlagEEBibTexAbstractModal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement
methodology. Despite its many advantages, the formalism as well as its currently known extensions are incapable of expressing
some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce
a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcomes
many of the limitations. We investigate the computational complexity of modal and thorough refinement checking on PMTS and
its subclasses and provide a direct encoding of the modal refinement problem into quantified Boolean formulae, allowing us
to employ state-of-the-art QBF solvers for modal refinement checking. The experiments we report on show that the feasibility
of refinement checking is more influenced by the degree of nondeterminism rather than by the syntactic restrictions on the
types of formulae allowed in the description of the PMTS.
[15]
TCTL-Preserving Translations from Timed-Arc Petri Nets to Networks of Timed AutomatabyJ. BygM. JacobsenL. JacobsenK.Y. JørgensenM.H. MøllerJ. SrbaTheoretical Computer Science
volume 5375ofpages 3--28Elsevier Science2014PDFElsevier ScienceEEBibTexAbstractWe present a framework for TCTL-preserving translations between time-dependent modelling formalisms. The framework guarantees
that once the original and the translated system are in one-by-many correspondence relation (a notion of behavioural equivalence
between timed transition systems) then TCTL properties of the original system can be transformed too while preserving the
verification answers. We demonstrate the usability of the technique on two reductions from bounded timed-arc Petri nets to
networks for timed automata, providing unified proofs of the translations implemented in the verification tool TAPAAL. We
evaluate the efficiency of the approach on a number of experiments: alternating bit protocol, Fischerʼs protocol, Lynch-Shavit
protocol, MPEG-2 encoder, engine workshop and medical workflow. The results are encouraging and confirm the practical applicability
of the approach.
[14]
Model-Checking Web Services Business Activity ProtocolsbyA.P. Marques Jr.A.P. RavnJ. SrbaS. VighioInternational Journal on Software Tools for Technology Transfer (STTT)
volume 152ofpages 125--147Springer-Verlag2013PDFSpringer-VerlagEEBibTexAbstractWeb Services Business Activity specification definestwo coordination protocols BAwCC (Business Agreement with Coordination
Completion)and BAwPC (Business Agreement with Participant Completion)that ensure a consistent agreement on the outcome of
long-running distributedapplications. In order to verify fundamental properties of the protocolswe provide formal analyses
in the model checker UPPAAL.Our analyses are supported by a newly developed tool chain,where in the first step we translatetables
with state-transition protocol descriptionsinto an intermediate XML format, and in the second step wetranslate this format
into a network of communicating state machinesdirectly suitable for verification in UPPAAL.Our results show that the WS-BA
protocols, as described in the standardspecification, violate correct operation by reaching invalid statesfor all underlying
communication media except for a perfect FIFO.Hence we propose changes to the protocols and a furtherinvestigation of the
modified protocols suggests that in case ofthe BAwCC protocol messages shouldbe received in the same order as they are sent
to preserve correct behaviour,while BAwPC is now correct even for asynchronous,unordered, lossy and duplicating media.Another
important property of communication protocolsis that all parties always reach, under certain fairness assumptions,their final
states. Based on an automatic verification with differentcommunication models, we prove that our enhanced protocols satisfy
thisproperty whereas the original protocols do not.All verification results presented in this article were performedin a fully
automatic way using our new tool csv2uppaal.
[13]
EXPTIME-Completeness of Thorough Refinement on Modal Transition SystemsbyN. BenesJ. KretinskyK.G. LarsenJ. SrbaInformation and Computation
volume 218ofpages 54--68Elsevier Science2012PDFElsevier ScienceEEBibTexAbstractModal transition systems (MTS), a specification formalism introduced more than 20 years ago, has recently received a considerable
attention in several different areas. Many of the fundamental questions related to MTSs have already been answered. However,
the problem of the exact computational complexity of thorough refinement checking between two finite MTSs remained unsolved.
We settle down this question by showing EXPTIME-completeness of thorough refinement checking on finite MTSs. The upper-bound
result relies on a novel algorithm running in single exponential time providing a direct goal-oriented way to decide thorough
refinement. If the right-hand side MTS is moreover deterministic, or has a fixed size, the running time of the algorithm becomes
polynomial. The lower-bound proof is achieved by reduction from the acceptance problem of alternating linear bounded automata
and the problem remains EXPTIME-hard even if the left-hand side MTS is fixed and deterministic.
[12]
Extending Modal Transition Systems with Structured LabelsbyS.S. BauerL. JuhlK.G. LarsenA. LegayJ. SrbaMathematical Structures in Computer Science
volume 224ofpages 581--617Cambridge University Press2012PDFCambridge University PressEEBibTexAbstractWe introduce a novel formalism of label-structured modal transition systems that combines the classical may/must modalities
on transitions with structured labels that represent quantitative aspects of the model. On the one hand, the specification
formalism is general enough to include models like weighted modal transition systems and allows the system developers to employ
more complex label refinement than in the previously studied theories. On the other hand, the formalism maintains the desirable
properties required by any specification theory supporting compositional reasoning. In particular, we study modal and thorough
refinement, determinization, parallel composition, conjunction, quotient, and logical characterization of label-structured
modal transition systems.
[11]
Modal Transition Systems with Weight IntervalsbyL. JuhlK.G. LarsenJ. SrbaJournal of Logic and Algebraic Programming
volume 814ofpages 408--421Elsevier Science2012PDFElsevier ScienceBibTexAbstractWe propose weighted modal transition systems, an extension to the well-studied specification formalism of modal transition
systems that allows to express both required and optional behaviours of their intended implementations. In our extension we
decorate each transition with a weight interval that indicates the range of concrete weight values available to the potential
implementations. In this way resource constraints can be modelled using the modal approach. We focus on two problems. First,
we study the question of existence/finding the largest common refinement for a number of finite deterministic specifications
and we show PSPACE-completeness of this problem. By constructing the most general common refinement, we allow for a stepwise
and iterative construction of a common implementation. Second, we study a logical characterisation of the formalism and show
that a formula in a natural weight extension of the logic CTL is satisfied by a given modal specification if and only if it
is satisfied by all its refinements. The weight extension is general enough to express different sorts of properties that
we want our weights to satisfy.
[10]
On Determinism in Modal Transition SystemsbyN. BenesJ. KretinskyK.G. LarsenJ. SrbaTheoretical Computer Science
volume 41041ofpages 4026--4043Elsevier Science2009PDFElsevier ScienceEEBibTexAbstractModal transition system (MTS) is a formalism which extends the classical notion of labelled transition systems by introducing
transitions of two types: must transitions that have to be present in any implementation of the MTS and may transitions that
are allowed but not required. The MTS framework has proved to be useful as a specification formalism of component-based systems
as it supports compositional verification and stepwise refinement. Nevertheless, there are some limitations of the theory,
namely that the naturally defined notions of modal refinement and modal composition are incomplete with respect to the semantic
view based on the sets of the implementations of a given MTS specification. Recent work indicates that some of these limitations
might be overcome by considering deterministic systems, which seem to be more manageable but still interesting for several
application areas. In the present article, we provide a comprehensive account of the MTS framework in the deterministic setting.
We study a number of problems previously considered on MTS and point out to what extend we can expect better results under
the restriction of determinism.
[9]
Beyond Language Equivalence on Visibly Pushdown AutomatabyJ. SrbaLogical Methods in Computer Science
volume 51:2ofpages 1--22Creative Commons2009PDFCreative CommonsEEBibTexAbstractWe study (bi)simulation-like preorder/equivalence checking on the class of visibly pushdown automata and its natural subclasses
visibly BPA (Basic Process Algebra) and visibly one-counter automata. We describe generic methods for proving complexity upper
and lower bounds for a number of studied preorders and equivalences like simulation, completed simulation, ready simulation,
2-nested simulation preorders/equivalences and bisimulation equivalence. Our main results are that all the mentioned equivalences
and preorders are EXPTIME-complete on visibly pushdown automata, PSPACE-complete on visibly one-counter automata and P-complete
on visibly BPA. Our PSPACE lower bound for visibly one-counter automata improves also the previously known DP-hardness results
for ordinary one-counter automata and one-counter nets. Finally, we study regularity checking problems for visibly pushdown
automata and show that they can be decided in polynomial time.
[8]
Undecidability of Bisimilarity by Defender's ForcingbyP. JancarJ. SrbaJournal of the ACM
volume 551ofpages 1--26ACM2008PDFACMEEBibTexAbstractStirling (1996, 1998) proved the decidability of bisimilarity on so-called normed pushdown processes. This result was substantially
extended by Senizergues(1998, 2005) who showed the decidability of bisimilarity for regular (or equational) graphs of finite
out-degree; this essentially coincides with weak bisimilarity of processes generated by (unnormed) pushdown automata where
the epsilon-transitions can only deterministically pop the stack. The question of decidability of bisimilarity for the more
general class of so called Type -1 systems, which is equivalent to weak bisimilarity on unrestricted epsilon-popping pushdown
processes, was left open. This was repeatedly indicated by both Stirling and Senizergues. Here we answer the question negatively,
that is, we show the undecidability of bisimilarity on Type -1 systems, even in the normed case. We achieve the result by
applying a technique we call Defender's Forcing, referring to the bisimulation games. The idea is simple, yet powerful. We
demonstrate its versatility by deriving further results in a uniform way. First, we classify several versions of the undecidable
problems for prefix rewrite systems (or pushdown automata) as Pi^0_1-complete or Sigma^1_1-complete. Second, we solve the
decidability question for weak bisimilarity on PA (Process Algebra) processes, showing that the problem is undecidable and
even Sigma^1_1-complete. Third, we show Sigma^1_1-completeness of weak bisimilarity for so-called parallel pushdown (or multiset)
automata, a subclass of (labeled, place/transition) Petri nets.
[7]
Decidability Issues for Extended Ping-Pong ProtocolsbyH. HüttelJ. SrbaJournal of Automated Reasoning
volume 361--2ofpages 125--147Kluwer2006PDFKluwerEEBibTexAbstractWe use some recent techniques from process algebra to draw several conclusions about the well studied class of ping-pong protocols
introduced by Dolev and Yao. In particular we show that all nontrivial properties, including reachability and equivalence
checking wrt. the whole van Glabbeek's spectrum, become undecidable for a very simple recursive extension of the protocol.
The result holds even if no nondeterministic choice operator is allowed but reachability is shown to be decidable in polynomial
time if only two parties are participating in the protocol. We also show that the calculus is capable of an implicit description
of the active intruder, including full analysis and synthesis of messages in the sense of Amadio, Lugiez and Vanackere. We
conclude by showing that reachability analysis for a replicative variant of the protocol becomes decidable.
[6]
On the Computational Complexity of Bisimulation, ReduxbyF. MollerS.A. SmolkaJ. SrbaInformation and Computation
volume 1922ofpages 129--143Elsevier Science2004PDFElsevier ScienceEEBibTexAbstractParis Kanellakis and the second author (Smolka) were among the first to investigate the computational complexity of bisimulation,
and the first and third authors (Moller and Srba) have long-established track records in the field. Smolka and Moller have
also written a brief survey about the computational complexity of bisimulation [Moller,Smolka'95]. The authors believe that
the special issue of Information and Computation devoted to PCK50: Principles of Computing and Knowledge: Paris C. Kanellakis
Memorial Workshop represents an ideal opportunity for an up-to-date look at the subject.
[5]
Roadmap of Infinite ResultsbyJ. SrbaBulletin of the European Association for Theoretical Computer Science, Columns: Concurrency
volume 78ofpages 163--1752002EEBibTexAbstractThis paper provides a comprehensive summary of equivalence checking results for infinite-state systems. References to the
relevant papers will be updated continuously according to the development in the area. The most recent version of this document
is available from the EE web-page.
[4]
Strong Bisimilarity of Simple Process Algebras: Complexity Lower BoundsbyJ. SrbaActa Informatica
volume 39ofpages 469--499Springer-Verlag2003PDFSpringer-VerlagEEBibTexAbstractWe study bisimilarity and regularity problems of simple process algebras. In particular, we show PSPACE-hardness of the following
problems: (i) strong bisimilarity of Basic Parallel Processes (BPP), (ii) strong bisimilarity of Basic Process Algebra (BPA),
(iii) strong regularity of BPP, and (iv) strong regularity of BPA. We also demonstrate NL-hardness of strong regularity problems
for the normed subclasses of BPP and BPA. Bisimilarity problems of simple process algebras are introduced in a general framework
of process rewrite systems, and a uniform description of the new techniques used for the hardness proofs is provided.
[3]
Undecidability of Domino Games and Hhp-BisimilaritybyM. JurdzinskiM. NielsenJ. SrbaInformation and Computation
volume 1842ofpages 343--368Elsevier Science2003PDFElsevier ScienceEEBibTexAbstract History preserving bisimilarity (hp-bisimilarity) and hereditary history preserving bisimilarity (hhp-bisimilarity) are behavioural
equivalences taking into account causal relationships between events of concurrent systems. Their prominent feature is that
they are preserved under action refinement, an operation important for the top-down design of concurrent systems. It is shown
that, in contrast to hp-bisimilarity, checking hhp-bisimilarity for finite labelled asyn\-chro\-nous transition systems is
undecidable, by a reduction from the halting problem of 2-counter machines. To make the proof more transparent a novel intermediate
problem of checking domino bisimilarity for origin constrained tiling systems is introduced and shown undecidable. It is also
shown that the unlabelled domino bisimilarity problem is undecidable, which implies undecidability of hhp-bisimilarity for
unlabelled finite asynchronous systems. Moreover, it is argued that the undecidability of hhp-bisimilarity holds for finite
elementary net systems and 1-safe Petri nets.
[2]
Complexity of Weak Bisimilarity and Regularity for BPA and BPPbyJ. SrbaMathematical Structures in Computer Science
volume 13ofpages 567--587Cambridge University Press2003PDFCambridge University PressEEBibTexAbstractIt is an open problem whether weak bisimilarity is decidable for Basic Process Algebra (BPA) and Basic Parallel Processes
(BPP). A PSPACE lower bound for BPA and NP lower bound for BPP were demonstrated by Stribrna. Mayr recently achieved a result,
saying that weak bisimilarity for BPP is a hard problem for the second level of polynomial hierarchy. We improve this lower
bound to PSPACE, moreover for the restricted class of normed BPP. Weak regularity (finiteness) of BPA and BPP is not known
to be decidable either. In the case of BPP there is a hardness result for the second level of arithmetical hierarchy by Mayr,
which we improve to PSPACE. No lower bound has previously been established for BPA. We demonstrate DP-hardness, which in particular
implies both NP and coNP-hardness. In each of the bisimulation/regularity problems we consider also the classes of normed
processes. Finally we show how the technique for proving co-NP lower bound for weak bisimilarity of BPA can be applied to
strong bisimilarity of BPP.
[1]
Basic Process Algebra with Deadlocking StatesbyJ. SrbaTheoretical Computer Science
volume 2661--2ofpages 605--630Elsevier Science2001PDFElsevier ScienceEEBibTexAbstractBisimilarity and regularity are decidable properties for the class of BPA (or context--free) processes. We extend BPA with
a deadlocking state obtaining BPAd systems. We show that the BPAd class is more expressive w.r.t. bisimilarity, but it remains
language equivalent to BPA. We prove that bisimilarity and regularity remain decidable for BPAd. Finally we give a characterisation
of those BPAd processes that can be equivalently (up to bisimilarity) described within the pure BPA syntax.
