Search

We consider the problem of responsibility attribution in the setting of parametric Markov chains. Given a family of Markov chains over a set of parameters, and a property, responsibility attribution asks how the difference in the value of the property should be attributed to the parameters when they change from one point in the parameter space to another. We formalize responsibility as path-based attribution schemes studied in cooperative game theory. An attribution scheme in a game determines how a value (a surplus or a cost) is distributed among a set of participants. Path-based attribution schemes include the well-studied Aumann-Shapley and the Shapley-Shubik schemes. In our context, an attribution scheme measures the responsibility of each parameter on the value function of the parametric Markov chain. We study the decision problem for path-based attribution schemes. Our main technical result is an algorithm for deciding if a path-based attribution scheme for a rational (ratios of polynomials) cost function is over a rational threshold. In particular, it is decidable if the Aumann-Shapley value for a player is at least a given rational number. As a consequence, we show that responsibility attribution is decidable for parametric Markov chains and for a general class of properties that include expectation and variance of discounted sum and long-run average rewards, as well as specifications in temporal logic.

This paper studies formal synthesis of controllers for continuous-spacesystems with unknown dynamics to satisfy requirements expressed as lineartemporal logic formulas. Formal abstraction-based synthesis schemes rely on aprecise mathematical model of the system to build a finite abstract model,which is then used to design a controller. The abstraction-based schemes arenot applicable when the dynamics of the system are unknown. We propose adata-driven approach that computes the growth bound of the system using afinite number of trajectories. The growth bound together with the sampledtrajectories are then used to construct the abstraction and synthesise acontroller. Our approach casts the computation of the growth bound as a robust convexoptimisation program (RCP). Since the unknown dynamics appear in theoptimisation, we formulate a scenario convex program (SCP) corresponding to theRCP using a finite number of sampled trajectories. We establish a samplecomplexity result that gives a lower bound for the number of sampledtrajectories to guarantee the correctness of the growth bound computed from theSCP with a given confidence. We also provide a sample complexity result for thesatisfaction of the specification on the system in closed loop with thedesigned controller for a given confidence. Our results are founded onestimating a bound on the Lipschitz constant of the system and provideguarantees on satisfaction of both finite and infinite-horizon specifications.We show that our data-driven approach can be readily used as a model-freeabstraction refinement scheme by modifying the formulation of the growth boundand providing similar sample complexity results. The performance of ourapproach is shown on three case studies.

Reachability problems in infinite-state systems are often subject to extremely high complexity. This motivates the investigation of efficient overapproximations, where we add transitions to obtain a system in which reachability can be decided more efficiently. We consider bidirected infinite-state systems, where for every transition there is a transition with opposite effect. We study bidirected reachability in the framework of valence systems, an abstract model featuring finitely many control states and an infinite-state storage that is specified by a finite graph. By picking suitable graphs, valence systems can uniformly model counters as in vector addition systems, pushdowns, integer counters, and combinations thereof. We provide a comprehensive complexity landscape for bidirected reachability and show that the complexity drops (often to polynomial time) from that of general reachability, for almost every storage mechanism where reachability is known to be decidable., 27 pages

The COVID-19 pandemic forced students and teachers to engage in emergency remote learning. Remote learning is particularly challenging for students and teachers in lowresource contexts. We aim to analyze the adaptation process of teachers who engaged in remote emergency teaching in low-resource contexts. We conduct ten interviews with teachers who provided emergency online teaching in Lebanon. We show that there was a decrease in synchronous student-teacher, student-content, and student-student interactions due to the scarcity of resources. We also show how the teachers adapted their practice to cope with these challenges, and how their adaptation process increased asynchronous student-teacher and student-content interactions., 28th International Conference on Computers in Education, 23-27 November 2020, Web conference.

Dynamic networks of concurrent pushdown systems (DCPS) are a theoretical model for multi-threaded recursive programs with shared global state and dynamical creation of threads. The (global) state reachability problem for DCPS is undecidable in general, but Atig et al. (2009) showed that it becomes decidable, and is in 2EXPSPACE, when each thread is restricted to a fixed number of context switches. The best known lower bound for the problem is EXPSPACE-hard and this lower bound follows already when each thread is a finite-state machine and runs atomically to completion (i.e., does not switch contexts). In this paper, we close the gap by showing that state reachability is 2EXPSPACE-hard already with only one context switch. Interestingly, state reachability analysis is in EXPSPACE both for pushdown threads without context switches as well as for finite-state threads with arbitrary context switches. Thus, recursive threads together with a single context switch provide an exponential advantage. Our proof techniques are of independent interest for 2EXPSPACE-hardness results. We introduce transducer-defined Petri nets, a succinct representation for Petri nets, and show coverability is 2EXPSPACE-hard for this model. To show 2EXPSPACE-hardness, we present a modified version of Lipton's simulation of counter machines by Petri nets, where the net programs can make explicit recursive procedure calls up to a bounded depth.

We present a new algorithm to solve the supervisory control problem over non-terminating processes modeled as $\omega$-regular automata. A solution to this problem was obtained by Thistle in 1995 which uses complex manipulations of automata. We show a new solution to the problem through a reduction to obliging games, which, in turn, can be reduced to $\omega$-regular reactive synthesis. Therefore, our reduction results in a symbolic algorithm based on manipulating sets of states using tools from reactive synthesis.

Probabilistic bisimulation is a fundamental notion of process equivalence for probabilistic systems. Among others, it has important applications including formalizing the anonymity property of several communication protocols. There is a lot of work on verifying probabilistic bisimulation for finite systems. This is however not the case for parameterized systems, where the problem is in general undecidable. In this paper we provide a generic framework for reasoning about probabilistic bisimulation for parameterized systems. Our approach is in the spirit of software verification, wherein we encode proof rules for probabilistic bisimulation and use a decidable first-order theory to specify systems and candidate bisimulation relations, which can then be checked automatically against the proof rules. As a case study, we show that our framework is sufficiently expressive for proving the anonymity property of the parameterized dining cryptographers protocol and the parameterized grades protocol, when supplied with a candidate regular bisimulation relation. Both of these protocols hitherto could not be verified by existing automatic methods. Moreover, with the help of standard automata learning algorithms, we show that the candidate relations can be synthesized fully automatically, making the verification fully automated.

Robotics applications involve programming concurrent components synchronising through messages while simultaneously executing motion primitives that control the state of the physical world. Today, these applications are typically programmed in low-level imperative programming languages which provide little support for abstraction or reasoning. We present a unifying programming model for concurrent message-passing systems that additionally control the evolution of physical state variables, together with a compositional reasoning framework based on multiparty session types. Our programming model combines message-passing concurrent processes with motion primitives. Processes represent autonomous components in a robotic assembly, such as a cart or a robotic arm, and they synchronise via discrete messages as well as via motion primitives. Continuous evolution of trajectories under the action of controllers is also modelled by motion primitives, which operate in global, physical time. We use multiparty session types as specifications to orchestrate discrete message-passing concurrency and continuous flow of trajectories. A global session type specifies the communication protocol among the components with joint motion primitives. A projection from a global type ensures that jointly executed actions at end-points are communication safe and deadlock-free, i.e., session-typed components do not get stuck. Together, these checks provide a compositional verification methodology for assemblies of robotic components with respect to concurrency invariants such as a progress property of communications as well as dynamic invariants such as absence of collision. We have implemented our core language and, through initial experiments, have shown how multiparty session types can be used to specify and compositionally verify robotic systems implemented on top of off-the-shelf and custom hardware using standard robotics application libraries.