Showing 1–14 of 14 results for author: Funke, F

Discussing Risks and Benefits in the Future of Hybrid Rehabilitation and Fitness in Mixed Reality

Authors: Jana Franceska Funke, Enrico Rukzio

Abstract: In a world where in-person context transitions more into remote and hybrid concepts, we should consider new concepts of interaction in health and rehabilitation and what advantages and disadvantages they bring. One of the rising topics is mixed reality, where we can use the advantages of immersive 3D, 360-degree environments. Meanwhile, physical activity is further decreasing and with it negative… ▽ More In a world where in-person context transitions more into remote and hybrid concepts, we should consider new concepts of interaction in health and rehabilitation and what advantages and disadvantages they bring. One of the rising topics is mixed reality, where we can use the advantages of immersive 3D, 360-degree environments. Meanwhile, physical activity is further decreasing and with it negative effects increase through sedentary behaviour or wrong and untrained movements. In this position paper, we discuss these new risks and potential benefits of mixed reality technology when used for rehabilitation and fitness. We conclude with suggesting better feedback and guidance for physical movement and tasks at home. Improving feedback and guidance for participants could be achieved through using new technologies like virtual reality and motion tracking. △ Less

Submitted 16 May, 2024; originally announced May 2024.

Comments: workshop paper

On probability-raising causality in Markov decision processes

Authors: Christel Baier, Florian Funke, Jakob Piribauer, Robin Ziemek

Abstract: The purpose of this paper is to introduce a notion of causality in Markov decision processes based on the probability-raising principle and to analyze its algorithmic properties. The latter includes algorithms for checking cause-effect relationships and the existence of probability-raising causes for given effect scenarios. Inspired by concepts of statistical analysis, we study quality measures (r… ▽ More The purpose of this paper is to introduce a notion of causality in Markov decision processes based on the probability-raising principle and to analyze its algorithmic properties. The latter includes algorithms for checking cause-effect relationships and the existence of probability-raising causes for given effect scenarios. Inspired by concepts of statistical analysis, we study quality measures (recall, coverage ratio and f-score) for causes and develop algorithms for their computation. Finally, the computational complexity for finding optimal causes with respect to these measures is analyzed. △ Less

Submitted 21 January, 2022; originally announced January 2022.

Comments: This is the extended version of a conference version accepted for publication at FoSSaCS 2022

Causality-Based Game Solving

Authors: Christel Baier, Norine Coenen, Bernd Finkbeiner, Florian Funke, Simon Jantsch, Julian Siber

Abstract: We present a causality-based algorithm for solving two-player reachability games represented by logical constraints. These games are a useful formalism to model a wide array of problems arising, e.g., in program synthesis. Our technique for solving these games is based on the notion of subgoals, which are slices of the game that the reachability player necessarily needs to pass through in order to… ▽ More We present a causality-based algorithm for solving two-player reachability games represented by logical constraints. These games are a useful formalism to model a wide array of problems arising, e.g., in program synthesis. Our technique for solving these games is based on the notion of subgoals, which are slices of the game that the reachability player necessarily needs to pass through in order to reach the goal. We use Craig interpolation to identify these necessary sets of moves and recursively slice the game along these subgoals. Our approach allows us to infer winning strategies that are structured along the subgoals. If the game is won by the reachability player, this is a strategy that progresses through the subgoals towards the final goal; if the game is won by the safety player, it is a permissive strategy that completely avoids a single subgoal. We evaluate our prototype implementation on a range of different games. On multiple benchmark families, our prototype scales dramatically better than previously available tools. △ Less

Submitted 29 May, 2021; originally announced May 2021.

Comments: 33rd International Conference on Computer-Aided Verification (CAV 2021)

From Verification to Causality-based Explications

Authors: Christel Baier, Clemens Dubslaff, Florian Funke, Simon Jantsch, Rupak Majumdar, Jakob Piribauer, Robin Ziemek

Abstract: In view of the growing complexity of modern software architectures, formal models are increasingly used to understand why a system works the way it does, opposed to simply verifying that it behaves as intended. This paper surveys approaches to formally explicate the observable behavior of reactive systems. We describe how Halpern and Pearl's notion of actual causation inspired verification-oriente… ▽ More In view of the growing complexity of modern software architectures, formal models are increasingly used to understand why a system works the way it does, opposed to simply verifying that it behaves as intended. This paper surveys approaches to formally explicate the observable behavior of reactive systems. We describe how Halpern and Pearl's notion of actual causation inspired verification-oriented studies of cause-effect relationships in the evolution of a system. A second focus lies on applications of the Shapley value to responsibility ascriptions, aimed to measure the influence of an event on an observable effect. Finally, formal approaches to probabilistic causation are collected and connected, and their relevance to the understanding of probabilistic systems is discussed. △ Less

Submitted 20 May, 2021; originally announced May 2021.

Comments: 20 pages, to appear in Proceedings of ICALP'21

A Game-Theoretic Account of Responsibility Allocation

Authors: Christel Baier, Florian Funke, Rupak Majumdar

Abstract: When designing or analyzing multi-agent systems, a fundamental problem is responsibility ascription: to specify which agents are responsible for the joint outcome of their behaviors and to which extent. We model strategic multi-agent interaction as an extensive form game of imperfect information and define notions of forward (prospective) and backward (retrospective) responsibility. Forward respon… ▽ More When designing or analyzing multi-agent systems, a fundamental problem is responsibility ascription: to specify which agents are responsible for the joint outcome of their behaviors and to which extent. We model strategic multi-agent interaction as an extensive form game of imperfect information and define notions of forward (prospective) and backward (retrospective) responsibility. Forward responsibility identifies the responsibility of a group of agents for an outcome along all possible plays, whereas backward responsibility identifies the responsibility along a given play. We further distinguish between strategic and causal backward responsibility, where the former captures the epistemic knowledge of players along a play, while the latter formalizes which players -- possibly unknowingly -- caused the outcome. A formal connection between forward and backward notions is established in the case of perfect recall. We further ascribe quantitative responsibility through cooperative game theory. We show through a number of examples that our approach encompasses several prior formal accounts of responsibility attribution. △ Less

Submitted 19 May, 2021; originally announced May 2021.

Comments: 20 pages, 3 figures, technical report associated with an IJCAI'21 publication

Probabilistic causes in Markov chains

Authors: Christel Baier, Florian Funke, Simon Jantsch, Jakob Piribauer, Robin Ziemek

Abstract: The paper studies a probabilistic notion of causes in Markov chains that relies on the counterfactuality principle and the probability-raising property. This notion is motivated by the use of causes for monitoring purposes where the aim is to detect faulty or undesired behaviours before they actually occur. A cause is a set of finite executions of the system after which the probability of the effe… ▽ More The paper studies a probabilistic notion of causes in Markov chains that relies on the counterfactuality principle and the probability-raising property. This notion is motivated by the use of causes for monitoring purposes where the aim is to detect faulty or undesired behaviours before they actually occur. A cause is a set of finite executions of the system after which the probability of the effect exceeds a given threshold. We introduce multiple types of costs that capture the consumption of resources from different perspectives, and study the complexity of computing cost-minimal causes. △ Less

Submitted 8 July, 2021; v1 submitted 28 April, 2021; originally announced April 2021.

Comments: Full version of a conference paper at ATVA'21; 26 pages, 9 figures

The Orbit Problem for Parametric Linear Dynamical Systems

Authors: Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Florian Luca, Joël Ouaknine, David Purser, Markus A. Whiteland, James Worrell

Abstract: We study a parametric version of the Kannan-Lipton Orbit Problem for linear dynamical systems. We show decidability in the case of one parameter and Skolem-hardness with two or more parameters. More precisely, consider a $d$-dimensional square matrix $M$ whose entries are algebraic functions in one or more real variables. Given initial and target vectors $u,v\in \mathbb{Q}^d$, the parametric poi… ▽ More We study a parametric version of the Kannan-Lipton Orbit Problem for linear dynamical systems. We show decidability in the case of one parameter and Skolem-hardness with two or more parameters. More precisely, consider a $d$-dimensional square matrix $M$ whose entries are algebraic functions in one or more real variables. Given initial and target vectors $u,v\in \mathbb{Q}^d$, the parametric point-to-point orbit problem asks whether there exist values of the parameters giving rise to a concrete matrix $N \in \mathbb{R}^{d\times d}$, and a positive integer $n\in \mathbb{N}$, such that $N^nu = v$. We show decidability for the case in which $M$ depends only upon a single parameter, and we exhibit a reduction from the well-known Skolem Problem for linear recurrence sequences, suggesting intractability in the case of two or more parameters. △ Less

Submitted 13 August, 2021; v1 submitted 21 April, 2021; originally announced April 2021.

Comments: Full version of the paper appearing at CONCUR 2021

Responsibility and verification: Importance value in temporal logics

Authors: Corto Mascle, Christel Baier, Florian Funke, Simon Jantsch, Stefan Kiefer

Abstract: We aim at measuring the influence of the nondeterministic choices of a part of a system on its ability to satisfy a specification. For this purpose, we apply the concept of Shapley values to verification as a means to evaluate how important a part of a system is. The importance of a component is measured by giving its control to an adversary, alone or along with other components, and testing wheth… ▽ More We aim at measuring the influence of the nondeterministic choices of a part of a system on its ability to satisfy a specification. For this purpose, we apply the concept of Shapley values to verification as a means to evaluate how important a part of a system is. The importance of a component is measured by giving its control to an adversary, alone or along with other components, and testing whether the system can still fulfill the specification. We study this idea in the framework of model-checking with various classical types of linear-time specification, and propose several ways to transpose it to branching ones. We also provide tight complexity bounds in almost every case. △ Less

Submitted 20 April, 2021; v1 submitted 12 February, 2021; originally announced February 2021.

Comments: 23 pages, 11 figures, full version of a conference paper accepted at LICS'21

Reachability in Dynamical Systems with Rounding

Authors: Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, Amaury Pouly, David Purser, Markus A. Whiteland

Abstract: We consider reachability in dynamical systems with discrete linear updates, but with fixed digital precision, i.e., such that values of the system are rounded at each step. Given a matrix $M \in \mathbb{Q}^{d \times d}$, an initial vector $x\in\mathbb{Q}^{d}$, a granularity $g\in \mathbb{Q}_+$ and a rounding operation $[\cdot]$ projecting a vector of $\mathbb{Q}^{d}$ onto another vector whose ever… ▽ More We consider reachability in dynamical systems with discrete linear updates, but with fixed digital precision, i.e., such that values of the system are rounded at each step. Given a matrix $M \in \mathbb{Q}^{d \times d}$, an initial vector $x\in\mathbb{Q}^{d}$, a granularity $g\in \mathbb{Q}_+$ and a rounding operation $[\cdot]$ projecting a vector of $\mathbb{Q}^{d}$ onto another vector whose every entry is a multiple of $g$, we are interested in the behaviour of the orbit $\mathcal{O}={<}[x], [M[x]],[M[M[x]]],\dots{>}$, i.e., the trajectory of a linear dynamical system in which the state is rounded after each step. For arbitrary rounding functions with bounded effect, we show that the complexity of deciding point-to-point reachability---whether a given target $y \in\mathbb{Q}^{d}$ belongs to $\mathcal{O}$---is PSPACE-complete for hyperbolic systems (when no eigenvalue of $M$ has modulus one). We also establish decidability without any restrictions on eigenvalues for several natural classes of rounding functions. △ Less

Submitted 28 September, 2020; originally announced September 2020.

Comments: To appear at FSTTCS'20

SWITSS: Computing Small Witnessing Subsystems

Authors: Simon Jantsch, Hans Harder, Florian Funke, Christel Baier

Abstract: Witnessing subsystems for probabilistic reachability thresholds in discrete Markovian models are an important concept both as diagnostic information on why a property holds, and as input to refinement algorithms. We present SWITSS, a tool for the computation of Small WITnessing SubSystems. SWITSS implements exact and heuristic approaches based on reducing the problem to (mixed integer) linear prog… ▽ More Witnessing subsystems for probabilistic reachability thresholds in discrete Markovian models are an important concept both as diagnostic information on why a property holds, and as input to refinement algorithms. We present SWITSS, a tool for the computation of Small WITnessing SubSystems. SWITSS implements exact and heuristic approaches based on reducing the problem to (mixed integer) linear programming. Returned subsystems can automatically be rendered graphically and are accompanied with a certificate which proves that the subsystem is indeed a witness. △ Less

Submitted 10 August, 2020; originally announced August 2020.

Comments: 9 pages; accepted for publication in the Proceedings of FMCAD'20 (https://fmcad.org/)

Minimal witnesses for probabilistic timed automata

Authors: Simon Jantsch, Florian Funke, Christel Baier

Abstract: Witnessing subsystems have proven to be a useful concept in the analysis of probabilistic systems, for example as diagnostic information on why a given property holds or as input to refinement algorithms. This paper introduces witnessing subsystems for reachability problems in probabilistic timed automata (PTA). Using a new operation on difference bounds matrices, it is shown how Farkas certificat… ▽ More Witnessing subsystems have proven to be a useful concept in the analysis of probabilistic systems, for example as diagnostic information on why a given property holds or as input to refinement algorithms. This paper introduces witnessing subsystems for reachability problems in probabilistic timed automata (PTA). Using a new operation on difference bounds matrices, it is shown how Farkas certificates of finite-state bisimulation quotients of a PTA can be translated into witnessing subsystems. We present algorithms for the computation of minimal witnessing subsystems under three notions of minimality, which capture the timed behavior from different perspectives, and discuss their complexity. △ Less

Submitted 1 July, 2020; originally announced July 2020.

Comments: 33 pages; conference version accepted for publication at ATVA'20

Farkas certificates and minimal witnesses for probabilistic reachability constraints

Authors: Florian Funke, Simon Jantsch, Christel Baier

Abstract: This paper introduces Farkas certificates for lower and upper bounds on minimal and maximal reachability probabilities in Markov decision processes (MDP), which we derive using an MDP-variant of Farkas' Lemma. The set of all such certificates is shown to form a polytope whose points correspond to witnessing subsystems of the model and the property. Using this correspondence we can translate the pr… ▽ More This paper introduces Farkas certificates for lower and upper bounds on minimal and maximal reachability probabilities in Markov decision processes (MDP), which we derive using an MDP-variant of Farkas' Lemma. The set of all such certificates is shown to form a polytope whose points correspond to witnessing subsystems of the model and the property. Using this correspondence we can translate the problem of finding minimal witnesses to the problem of finding vertices with a maximal number of zeros. While computing such vertices is computationally hard in general, we derive new heuristics from our formulations that exhibit competitive performance compared to state-of-the-art techniques. As an argument that asymptotically better algorithms cannot be hoped for, we show that the decision version of finding minimal witnesses is NP-complete even for acyclic Markov chains. △ Less

Submitted 5 February, 2020; v1 submitted 23 October, 2019; originally announced October 2019.

Comments: 41 pages, 7 figures (including appendix), to appear in TACAS 2020

Compacting Transactional Data in Hybrid OLTP & OLAP Databases

Authors: Florian Funke, Alfons Kemper, Thomas Neumann

Abstract: Growing main memory sizes have facilitated database management systems that keep the entire database in main memory. The drastic performance improvements that came along with these in-memory systems have made it possible to reunite the two areas of online transaction processing (OLTP) and online analytical processing (OLAP): An emerging class of hybrid OLTP and OLAP database systems allows to proc… ▽ More Growing main memory sizes have facilitated database management systems that keep the entire database in main memory. The drastic performance improvements that came along with these in-memory systems have made it possible to reunite the two areas of online transaction processing (OLTP) and online analytical processing (OLAP): An emerging class of hybrid OLTP and OLAP database systems allows to process analytical queries directly on the transactional data. By offering arbitrarily current snapshots of the transactional data for OLAP, these systems enable real-time business intelligence. Despite memory sizes of several Terabytes in a single commodity server, RAM is still a precious resource: Since free memory can be used for intermediate results in query processing, the amount of memory determines query performance to a large extent. Consequently, we propose the compaction of memory-resident databases. Compaction consists of two tasks: First, separating the mutable working set from the immutable "frozen" data. Second, compressing the immutable data and optimizing it for efficient, memory-consumption-friendly snapshotting. Our approach reorganizes and compresses transactional data online and yet hardly affects the mission-critical OLTP throughput. This is achieved by unburdening the OLTP threads from all additional processing and performing these tasks asynchronously. △ Less

Submitted 1 August, 2012; originally announced August 2012.

Comments: VLDB2012

Journal ref: Proceedings of the VLDB Endowment (PVLDB), Vol. 5, No. 11, pp. 1424-1435 (2012)

Automated derivation of the adjoint of high-level transient finite element programs

Authors: Patrick E. Farrell, David A. Ham, Simon F. Funke, Marie E. Rognes

Abstract: In this paper we demonstrate a new technique for deriving discrete adjoint and tangent linear models of finite element models. The technique is significantly more efficient and automatic than standard algorithmic differentiation techniques. The approach relies on a high-level symbolic representation of the forward problem. In contrast to develo** a model directly in Fortran or C++, high-level sy… ▽ More In this paper we demonstrate a new technique for deriving discrete adjoint and tangent linear models of finite element models. The technique is significantly more efficient and automatic than standard algorithmic differentiation techniques. The approach relies on a high-level symbolic representation of the forward problem. In contrast to develo** a model directly in Fortran or C++, high-level systems allow the developer to express the variational problems to be solved in near-mathematical notation. As such, these systems have a key advantage: since the mathematical structure of the problem is preserved, they are more amenable to automated analysis and manipulation. The framework introduced here is implemented in a freely available software package named dolfin-adjoint, based on the FEniCS Project. Our approach to automated adjoint derivation relies on run-time annotation of the temporal structure of the model, and employs the FEniCS finite element form compiler to automatically generate the low-level code for the derived models. The approach requires only trivial changes to a large class of forward models, including complicated time-dependent nonlinear models. The adjoint model automatically employs optimal checkpointing schemes to mitigate storage requirements for nonlinear models, without any user management or intervention. Furthermore, both the tangent linear and adjoint models naturally work in parallel, without any need to differentiate through calls to MPI or to parse OpenMP directives. The generality, applicability and efficiency of the approach are demonstrated with examples from a wide range of scientific applications. △ Less

Submitted 16 October, 2013; v1 submitted 25 April, 2012; originally announced April 2012.

MSC Class: 65N30; 68N20; 49M29

Journal ref: SIAM Journal on Scientific Computing 2013 35:4, C369-C393