Showing 1–18 of 18 results for author: Sedwards, S

SOAP: Cross-sensor Domain Adaptation for 3D Object Detection Using Stationary Object Aggregation Pseudo-labelling

Authors: Chengjie Huang, Vahdat Abdelzad, Sean Sedwards, Krzysztof Czarnecki

Abstract: We consider the problem of cross-sensor domain adaptation in the context of LiDAR-based 3D object detection and propose Stationary Object Aggregation Pseudo-labelling (SOAP) to generate high quality pseudo-labels for stationary objects. In contrast to the current state-of-the-art in-domain practice of aggregating just a few input scans, SOAP aggregates entire sequences of point clouds at the input… ▽ More We consider the problem of cross-sensor domain adaptation in the context of LiDAR-based 3D object detection and propose Stationary Object Aggregation Pseudo-labelling (SOAP) to generate high quality pseudo-labels for stationary objects. In contrast to the current state-of-the-art in-domain practice of aggregating just a few input scans, SOAP aggregates entire sequences of point clouds at the input level to reduce the sensor domain gap. Then, by means of what we call quasi-stationary training and spatial consistency post-processing, the SOAP model generates accurate pseudo-labels for stationary objects, closing a minimum of 30.3% domain gap compared to few-frame detectors. Our results also show that state-of-the-art domain adaptation approaches can achieve even greater performance in combination with SOAP, in both the unsupervised and semi-supervised settings. △ Less

Submitted 8 January, 2024; originally announced January 2024.

Comments: Accepted by WACV 2024

A Hierarchical Pedestrian Behavior Model to Generate Realistic Human Behavior in Traffic Simulation

Authors: Scott Larter, Rodrigo Queiroz, Sean Sedwards, Atrisha Sarkar, Krzysztof Czarnecki

Abstract: Modelling pedestrian behavior is crucial in the development and testing of autonomous vehicles. In this work, we present a hierarchical pedestrian behavior model that generates high-level decisions through the use of behavior trees, in order to produce maneuvers executed by a low-level motion planner using an adapted Social Force model. A full implementation of our work is integrated into GeoScena… ▽ More Modelling pedestrian behavior is crucial in the development and testing of autonomous vehicles. In this work, we present a hierarchical pedestrian behavior model that generates high-level decisions through the use of behavior trees, in order to produce maneuvers executed by a low-level motion planner using an adapted Social Force model. A full implementation of our work is integrated into GeoScenario Server, a scenario definition and execution engine, extending its vehicle simulation capabilities with pedestrian simulation. The extended environment allows simulating test scenarios involving both vehicles and pedestrians to assist in the scenario-based testing process of autonomous vehicles. The presented hierarchical model is evaluated on two real-world data sets collected at separate locations with different road structures. Our model is shown to replicate the real-world pedestrians' trajectories with a high degree of fidelity and a decision-making accuracy of 98% or better, given only high-level routing information for each pedestrian. △ Less

Submitted 31 May, 2022; originally announced June 2022.

Comments: 9 pages, 4 figures, 3 tables. Accepted to the 2022 IEEE Intelligent Vehicles Symposium

Recursive Constraints to Prevent Instability in Constrained Reinforcement Learning

Authors: Jaeyoung Lee, Sean Sedwards, Krzysztof Czarnecki

Abstract: We consider the challenge of finding a deterministic policy for a Markov decision process that uniformly (in all states) maximizes one reward subject to a probabilistic constraint over a different reward. Existing solutions do not fully address our precise problem definition, which nevertheless arises naturally in the context of safety-critical robotic systems. This class of problem is known to be… ▽ More We consider the challenge of finding a deterministic policy for a Markov decision process that uniformly (in all states) maximizes one reward subject to a probabilistic constraint over a different reward. Existing solutions do not fully address our precise problem definition, which nevertheless arises naturally in the context of safety-critical robotic systems. This class of problem is known to be hard, but the combined requirements of determinism and uniform optimality can create learning instability. In this work, after describing and motivating our problem with a simple example, we present a suitable constrained reinforcement learning algorithm that prevents learning instability, using recursive constraints. Our proposed approach admits an approximative form that improves efficiency and is conservative w.r.t. the constraint. △ Less

Submitted 19 January, 2022; originally announced January 2022.

Comments: Accepted at 1st Multi-Objective Decision Making Workshop (MODeM 2021). Cite as: Jaeyoung Lee, Sean Sedwards and Krzysztof Czarnecki. (2021). Recursive constraints to prevent instability in constrained reinforcement learning. In: Proc. 1st Multi-Objective Decision Making Workshop (MODeM 2021), Hayes, Mannion, Vamplew (eds). Online at http://modem2021.cs.nuigalway.ie

MSC Class: 68T05 ACM Class: I.2.6

Design Space of Behaviour Planning for Autonomous Driving

Authors: Marko Ilievski, Sean Sedwards, Ashish Gaurav, Aravind Balakrishnan, Atrisha Sarkar, Jaeyoung Lee, Frédéric Bouchard, Ryan De Iaco, Krzysztof Czarnecki

Abstract: We explore the complex design space of behaviour planning for autonomous driving. Design choices that successfully address one aspect of behaviour planning can critically constrain others. To aid the design process, in this work we decompose the design space with respect to important choices arising from the current state of the art approaches, and describe the resulting trade-offs. In doing this,… ▽ More We explore the complex design space of behaviour planning for autonomous driving. Design choices that successfully address one aspect of behaviour planning can critically constrain others. To aid the design process, in this work we decompose the design space with respect to important choices arising from the current state of the art approaches, and describe the resulting trade-offs. In doing this, we also identify interesting directions of future work. △ Less

Submitted 21 August, 2019; originally announced August 2019.

Comments: 8 pages, 6 figures

WiseMove: A Framework for Safe Deep Reinforcement Learning for Autonomous Driving

Authors: Jaeyoung Lee, Aravind Balakrishnan, Ashish Gaurav, Krzysztof Czarnecki, Sean Sedwards

Abstract: Machine learning can provide efficient solutions to the complex problems encountered in autonomous driving, but ensuring their safety remains a challenge. A number of authors have attempted to address this issue, but there are few publicly-available tools to adequately explore the trade-offs between functionality, scalability, and safety. We thus present WiseMove, a software framework to investi… ▽ More Machine learning can provide efficient solutions to the complex problems encountered in autonomous driving, but ensuring their safety remains a challenge. A number of authors have attempted to address this issue, but there are few publicly-available tools to adequately explore the trade-offs between functionality, scalability, and safety. We thus present WiseMove, a software framework to investigate safe deep reinforcement learning in the context of motion planning for autonomous driving. WiseMove adopts a modular learning architecture that suits our current research questions and can be adapted to new technologies and new questions. We present the details of WiseMove, demonstrate its use on a common traffic scenario, and describe how we use it in our ongoing safe learning research. △ Less

Submitted 11 February, 2019; originally announced February 2019.

Journal ref: International Conference on Quantitative Evaluation of Systems (QEST 2019)

Fast Falsification of Hybrid Systems using Probabilistically Adaptive Input

Authors: Gidon Ernst, Sean Sedwards, Zhenya Zhang, Ichiro Hasuo

Abstract: We present an algorithm that quickly finds falsifying inputs for hybrid systems, i.e., inputs that steer the system towards violation of a given temporal logic requirement. Our method is based on a probabilistically directed search of an increasingly fine grained spatial and temporal discretization of the input space. A key feature is that it adapts to the difficulty of a problem at hand, specific… ▽ More We present an algorithm that quickly finds falsifying inputs for hybrid systems, i.e., inputs that steer the system towards violation of a given temporal logic requirement. Our method is based on a probabilistically directed search of an increasingly fine grained spatial and temporal discretization of the input space. A key feature is that it adapts to the difficulty of a problem at hand, specifically to the local complexity of each input segment, as needed for falsification. In experiments with standard benchmarks, our approach consistently outperforms existing techniques by a significant margin. In recognition of the way it works and to distinguish it from previous work, we describe our method as a "Las Vegas tree search". △ Less

Submitted 10 December, 2018; originally announced December 2018.

Two-Layered Falsification of Hybrid Systems guided by Monte Carlo Tree Search

Authors: Zhenya Zhang, Gidon Ernst, Sean Sedwards, Paolo Arcaini, Ichiro Hasuo

Abstract: Few real-world hybrid systems are amenable to formal verification, due to their complexity and black box components. Optimization-based falsification---a methodology of search-based testing that employs stochastic optimization---is attracting attention as an alternative quality assurance method. Inspired by the recent works that advocate coverage and exploration in falsification, we introduce a tw… ▽ More Few real-world hybrid systems are amenable to formal verification, due to their complexity and black box components. Optimization-based falsification---a methodology of search-based testing that employs stochastic optimization---is attracting attention as an alternative quality assurance method. Inspired by the recent works that advocate coverage and exploration in falsification, we introduce a two-layered optimization framework that uses Monte Carlo tree search (MCTS), a popular machine learning technique with solid mathematical and empirical foundations. MCTS is used in the upper layer of our framework; it guides the lower layer of local hill-climbing optimization, thus balancing exploration and exploitation in a disciplined manner. △ Less

Submitted 12 August, 2018; v1 submitted 16 March, 2018; originally announced March 2018.

Time-Staging Enhancement of Hybrid System Falsification

Authors: Gidon Ernst, Ichiro Hasuo, Zhenya Zhang, Sean Sedwards

Abstract: Optimization-based falsification employs stochastic optimization algorithms to search for error input of hybrid systems. In this paper we introduce a simple idea to enhance falsification, namely time staging, that allows the time-causal structure of time-dependent signals to be exploited by the optimizers. Time staging consists of running a falsification solver multiple times, from one interval to… ▽ More Optimization-based falsification employs stochastic optimization algorithms to search for error input of hybrid systems. In this paper we introduce a simple idea to enhance falsification, namely time staging, that allows the time-causal structure of time-dependent signals to be exploited by the optimizers. Time staging consists of running a falsification solver multiple times, from one interval to another, incrementally constructing an input signal candidate. Our experiments show that time staging can dramatically increase performance in some realistic examples. We also present theoretical results that suggest the kinds of models and specifications for which time staging is likely to be effective. △ Less

Submitted 14 July, 2022; v1 submitted 10 March, 2018; originally announced March 2018.

Comments: In Proceedings SNR 2021, arXiv:2207.04391

Journal ref: EPTCS 361, 2022, pp. 25-43

Bounding Errors Due to Switching Delays in Incrementally Stable Switched Systems (Extended Version)

Authors: Kengo Kido, Sean Sedwards, Ichiro Hasuo

Abstract: Time delays pose an important challenge in networked control systems, which are now ubiquitous. Focusing on switched systems, we introduce a framework that provides an upper bound for errors caused by switching delays. Our framework is based on approximate bisimulation, a notion that has been previously utilized mainly for symbolic (discrete) abstraction of state spaces. Notable in our framework i… ▽ More Time delays pose an important challenge in networked control systems, which are now ubiquitous. Focusing on switched systems, we introduce a framework that provides an upper bound for errors caused by switching delays. Our framework is based on approximate bisimulation, a notion that has been previously utilized mainly for symbolic (discrete) abstraction of state spaces. Notable in our framework is that, in deriving an approximate bisimulation and thus an error bound, we use a simple incremental stability assumption (namely δ-GUAS) that does not itself refer to time delays. That this is the same assumption used for state-space discretization enables a two-step workflow for control synthesis for switched systems, in which a single Lyapunov-type stability witness serves for two different purposes of state discretization and co** with time delays. We demonstrate the proposed framework with a boost DC-DC converter, a common example of switched systems. △ Less

Submitted 23 December, 2017; v1 submitted 18 December, 2017; originally announced December 2017.

A Hierarchy of Scheduler Classes for Stochastic Automata

Authors: Pedro R. D'Argenio, Marcus Gerhold, Arnd Hartmanns, Sean Sedwards

Abstract: Stochastic automata are a formal compositional model for concurrent stochastic timed systems, with general distributions and non-deterministic choices. Measures of interest are defined over schedulers that resolve the nondeterminism. In this paper we investigate the power of various theoretically and practically motivated classes of schedulers, considering the classic complete-information view and… ▽ More Stochastic automata are a formal compositional model for concurrent stochastic timed systems, with general distributions and non-deterministic choices. Measures of interest are defined over schedulers that resolve the nondeterminism. In this paper we investigate the power of various theoretically and practically motivated classes of schedulers, considering the classic complete-information view and a restriction to non-prophetic schedulers. We prove a hierarchy of scheduler classes w.r.t. unbounded probabilistic reachability. We find that, unlike Markovian formalisms, stochastic automata distinguish most classes even in this basic setting. Verification and strategy synthesis methods thus face a tradeoff between powerful and efficient classes. Using lightweight scheduler sampling, we explore this tradeoff and demonstrate the concept of a useful approximative verification technique for stochastic automata. △ Less

Submitted 16 October, 2017; originally announced October 2017.

Distributed Verification of Rare Properties using Importance Splitting Observers

Authors: Cyrille Jegourel, Axel Legay, Sean Sedwards, Louis-Marie Traonouez

Abstract: Rare properties remain a challenge for statistical model checking (SMC) due to the quadratic scaling of variance with rarity. We address this with a variance reduction framework based on lightweight importance splitting observers. These expose the model-property automaton to allow the construction of score functions for high performance algorithms. The confidence intervals defined for importance… ▽ More Rare properties remain a challenge for statistical model checking (SMC) due to the quadratic scaling of variance with rarity. We address this with a variance reduction framework based on lightweight importance splitting observers. These expose the model-property automaton to allow the construction of score functions for high performance algorithms. The confidence intervals defined for importance splitting make it appealing for SMC, but optimising its performance in the standard way makes distribution inefficient. We show how it is possible to achieve equivalently good results in less time by distributing simpler algorithms. We first explore the challenges posed by importance splitting and present an algorithm optimised for distribution. We then define a specific bounded time logic that is compiled into memory-efficient observers to monitor executions. Finally, we demonstrate our framework on a number of challenging case studies. △ Less

Submitted 28 April, 2015; v1 submitted 6 February, 2015; originally announced February 2015.

Lightweight Monte Carlo Verification of Markov Decision Processes with Rewards

Authors: Axel Legay, Sean Sedwards, Louis-Marie Traonouez

Abstract: Markov decision processes are useful models of concurrency optimisation problems, but are often intractable for exhaustive verification methods. Recent work has introduced lightweight approximative techniques that sample directly from scheduler space, bringing the prospect of scalable alternatives to standard numerical model checking algorithms. The focus so far has been on optimising the probabil… ▽ More Markov decision processes are useful models of concurrency optimisation problems, but are often intractable for exhaustive verification methods. Recent work has introduced lightweight approximative techniques that sample directly from scheduler space, bringing the prospect of scalable alternatives to standard numerical model checking algorithms. The focus so far has been on optimising the probability of a property, but many problems require quantitative analysis of rewards. In this work we therefore present lightweight statistical model checking algorithms to optimise the rewards of Markov decision processes. We consider the standard definitions of rewards used in model checking, introducing an auxiliary hypothesis test to accommodate reachability rewards. We demonstrate the performance of our approach on a number of standard case studies. △ Less

Submitted 23 March, 2015; v1 submitted 20 October, 2014; originally announced October 2014.

Comments: 16 pages, 4 figures, 1 table

Smart Sampling for Lightweight Verification of Markov Decision Processes

Authors: Pedro D'Argenio, Axel Legay, Sean Sedwards, Louis-Marie Traonouez

Abstract: Markov decision processes (MDP) are useful to model optimisation problems in concurrent systems. To verify MDPs with efficient Monte Carlo techniques requires that their nondeterminism be resolved by a scheduler. Recent work has introduced the elements of lightweight techniques to sample directly from scheduler space, but finding optimal schedulers by simple sampling may be inefficient. Here we de… ▽ More Markov decision processes (MDP) are useful to model optimisation problems in concurrent systems. To verify MDPs with efficient Monte Carlo techniques requires that their nondeterminism be resolved by a scheduler. Recent work has introduced the elements of lightweight techniques to sample directly from scheduler space, but finding optimal schedulers by simple sampling may be inefficient. Here we describe "smart" sampling algorithms that can make substantial improvements in performance. △ Less

Submitted 4 February, 2015; v1 submitted 7 September, 2014; originally announced September 2014.

Comments: IEEE conference style, 11 pages, 5 algorithms, 11 figures, 1 table

Scalable Verification of Markov Decision Processes

Authors: Axel Legay, Sean Sedwards, Louis-Marie Traonouez

Abstract: Markov decision processes (MDP) are useful to model concurrent process optimisation problems, but verifying them with numerical methods is often intractable. Existing approximative approaches do not scale well and are limited to memoryless schedulers. Here we present the basis of scalable verification for MDPSs, using an O(1) memory representation of history-dependent schedulers. We thus facilitat… ▽ More Markov decision processes (MDP) are useful to model concurrent process optimisation problems, but verifying them with numerical methods is often intractable. Existing approximative approaches do not scale well and are limited to memoryless schedulers. Here we present the basis of scalable verification for MDPSs, using an O(1) memory representation of history-dependent schedulers. We thus facilitate scalable learning techniques and the use of massively parallel verification. △ Less

Submitted 17 September, 2014; v1 submitted 14 October, 2013; originally announced October 2013.

Comments: V4: FMDS version, 12 pages, 4 figures

Cooperation and competition in the dynamics of tissue architecture during homeostasis and tumorigenesis

Authors: Attila Csikász-Nagy, Luis M. Escudero, Martial Guillaud, Sean Sedwards, Buzz Baum, Matteo Cavaliere

Abstract: The construction of a network of cell-to-cell contacts makes it possible to characterize the patterns and spatial organisation of tissues. Such networks are highly dynamic, depending on the changes of the tissue architecture caused by cell division, death and migration. Local competitive and cooperative cell-to-cell interactions influence the choices cells make. We review the literature on quantit… ▽ More The construction of a network of cell-to-cell contacts makes it possible to characterize the patterns and spatial organisation of tissues. Such networks are highly dynamic, depending on the changes of the tissue architecture caused by cell division, death and migration. Local competitive and cooperative cell-to-cell interactions influence the choices cells make. We review the literature on quantitative data of epithelial tissue topology and present a dynamical network model that can be used to explore the evolutionary dynamics of a two dimensional tissue architecture with arbitrary cell-to-cell interactions. In particular, we show that various forms of experimentally observed types of interactions can be modelled using game theory. We discuss a model of cooperative and non-cooperative cell-to-cell communication that can capture the interplay between cellular competition and tissue dynamics. We conclude with an outlook on the possible uses of this approach in modelling tumorigenesis and tissue homeostasis. △ Less

Submitted 24 June, 2013; v1 submitted 31 May, 2013; originally announced May 2013.

Comments: 11 pages, 5 figures; Seminars in Cancer Biology (2013)

Statistical Model Checking for Stochastic Hybrid Systems

Authors: Alexandre David, Dehui Du, Kim G. Larsen, Axel Legay, Marius Mikučionis, Danny Bøgsted Poulsen, Sean Sedwards

Abstract: This paper presents novel extensions and applications of the UPPAAL-SMC model checker. The extensions allow for statistical model checking of stochastic hybrid systems. We show how our race-based stochastic semantics extends to networks of hybrid systems, and indicate the integration technique applied for implementing this semantics in the UPPAAL-SMC simulation engine. We r… ▽ More This paper presents novel extensions and applications of the UPPAAL-SMC model checker. The extensions allow for statistical model checking of stochastic hybrid systems. We show how our race-based stochastic semantics extends to networks of hybrid systems, and indicate the integration technique applied for implementing this semantics in the UPPAAL-SMC simulation engine. We report on two applications of the resulting tool-set coming from systems biology and energy aware buildings. △ Less

Submitted 19 August, 2012; originally announced August 2012.

Comments: In Proceedings HSB 2012, arXiv:1208.3151

ACM Class: D.2.4; D.2.5; G.3

Journal ref: EPTCS 92, 2012, pp. 122-136

Cross-entropy optimisation of importance sampling parameters for statistical model checking

Authors: Cyrille Jégourel, Axel Legay, Sean Sedwards

Abstract: Statistical model checking avoids the exponential growth of states associated with probabilistic model checking by estimating properties from multiple executions of a system and by giving results within confidence bounds. Rare properties are often very important but pose a particular challenge for simulation-based approaches, hence a key objective under these circumstances is to reduce the number… ▽ More Statistical model checking avoids the exponential growth of states associated with probabilistic model checking by estimating properties from multiple executions of a system and by giving results within confidence bounds. Rare properties are often very important but pose a particular challenge for simulation-based approaches, hence a key objective under these circumstances is to reduce the number and length of simulations necessary to produce a given level of confidence. Importance sampling is a well-established technique that achieves this, however to maintain the advantages of statistical model checking it is necessary to find good importance sampling distributions without considering the entire state space. Motivated by the above, we present a simple algorithm that uses the notion of cross-entropy to find the optimal parameters for an importance sampling distribution. In contrast to previous work, our algorithm uses a low dimensional vector of parameters to define this distribution and thus avoids the often intractable explicit representation of a transition matrix. We show that our parametrisation leads to a unique optimum and can produce many orders of magnitude improvement in simulation efficiency. We demonstrate the efficacy of our methodology by applying it to models from reliability engineering and biochemistry. △ Less

Submitted 25 January, 2012; originally announced January 2012.

Comments: 16 pages, 8 figures, LNCS style

Prosperity is associated with instability in dynamical networks

Authors: Matteo Cavaliere, Sean Sedwards, Corina E. Tarnita, Martin A. Nowak, Attila Csikász-Nagy

Abstract: Social, biological and economic networks grow and decline with occasional fragmentation and re-formation, often explained in terms of external perturbations. We show that these phenomena can be a direct consequence of simple imitation and internal conflicts between 'cooperators' and 'defectors'. We employ a game-theoretic model of dynamic network formation where successful individuals are more lik… ▽ More Social, biological and economic networks grow and decline with occasional fragmentation and re-formation, often explained in terms of external perturbations. We show that these phenomena can be a direct consequence of simple imitation and internal conflicts between 'cooperators' and 'defectors'. We employ a game-theoretic model of dynamic network formation where successful individuals are more likely to be imitated by newcomers who adopt their strategies and copy their social network. We find that, despite using the same mechanism, cooperators promote well-connected highly prosperous networks and defectors cause the network to fragment and lose its prosperity; defectors are unable to maintain the highly connected networks they invade. Once the network is fragmented it can be reconstructed by a new invasion of cooperators, leading to the cycle of formation and fragmentation seen, for example, in bacterial communities and socio-economic networks. In this endless struggle between cooperators and defectors we observe that cooperation leads to prosperity, but prosperity is associated with instability. Cooperation is prosperous when the network has frequent formation and fragmentation. △ Less

Submitted 27 September, 2011; v1 submitted 24 February, 2011; originally announced February 2011.

Comments: 49 pages, 10 figures; Journal of Theoretical Biology (2011)

MSC Class: 91A22