SearcharxivSearch

arXiv subjects

Jan Oliver Ringert

Publications and source records attributed to Jan Oliver Ringert.

At least 19 recordsLinked to original sources

Model Predictive Control for Crowd Navigation via Learning-Based Trajectory Prediction

Safe navigation in pedestrian-rich environments remains a key challenge for autonomous robots. This work evaluates the integration of a deep learning-based Social-Implicit (SI) pedestrian trajectory predictor within a Model Predictive Control (MPC) framework on the physical Continental Corriere robot. Tested across varied pedestrian densities, the SI-MPC system is compared to a traditional Constant Velocity (CV) model in both open-loop prediction and closed-loop navigation. Results show that SI improves trajectory prediction - reducing errors by up to 76% in low-density settings - and enhances safety and motion smoothness in crowded scenes. Moreover, real-world deployment reveals discrepancies between open-loop metrics and closed-loop performance, as the SI model yields broader, more cautious predictions. These findings emphasize the importance of system-level evaluation and highlight the SI-MPC framework's promise for safer, more adaptive navigation in dynamic, human-populated environments.

cs.RO

On Specifying for Trustworthiness

As autonomous systems (AS) increasingly become part of our daily lives, ensuring their trustworthiness is crucial. In order to demonstrate the trustworthiness of an AS, we first need to specify what is required for an AS to be considered trustworthy. This roadmap paper identifies key challenges for specifying for trustworthiness in AS, as identified during the "Specifying for Trustworthiness" workshop held as part of the UK Research and Innovation (UKRI) Trustworthy Autonomous Systems (TAS) programme. We look across a range of AS domains with consideration of the resilience, trust, functionality, verifiability, security, and governance and regulation of AS and identify some of the key specification challenges in these domains. We then highlight the intellectual challenges that are involved with specifying for trustworthiness in AS that cut across domains and are exacerbated by the inherent uncertainty involved with the environments in which AS need to operate.

cs.AI

Energy mu-Calculus: Symbolic Fixed-Point Algorithms for omega-Regular Energy Games

$ω$-regular energy games, which are weighted two-player turn-based games with the quantitative objective to keep the energy levels non-negative, have been used in the context of verification and synthesis. The logic of modal $μ$-calculus, when applied over game graphs with $ω$-regular winning conditions, allows defining symbolic algorithms in the form of fixed-point formulas for computing the sets of winning states. In this paper, we introduce energy $μ$-calculus, a multi-valued extension of the $μ$-calculus that serves as a symbolic framework for solving $ω$-regular energy games. Energy $μ$-calculus enables the seamless reuse of existing, well-known symbolic $μ$-calculus algorithms for $ω$-regular games, to solve their corresponding energy augmented variants. We define the syntax and semantics of energy $μ$-calculus over symbolic representations of the game graphs, and show how to use it to solve the decision and the minimum credit problems for $ω$-regular energy games, for both bounded and unbounded energy level accumulations.

cs.LO

Spectra: A Specification Language for Reactive Systems

Spectra is a new specification language for reactive systems, specifically tailored for the context of reactive synthesis. The meaning of Spectra is defined by a translation to a kernel language. Spectra comes with the Spectra Tools, a set of analyses, including a synthesizer to obtain a correct-by-construction implementation, several means for executing the resulting controller, and additional analyses aimed at helping engineers write higher-quality specifications. We present the language and give an overview of the tool set.

cs.SE

Performance Heuristics for GR(1) Synthesis and Related Algorithms

Reactive synthesis for the GR(1) fragment of LTL has been implemented and studied in many works. In this workshop paper we present and evaluate a list of heuristics to potentially reduce running times for GR(1) synthesis and related algorithms. The list includes early detection of fixed-points and unrealizability, fixed-point recycling, and heuristics for unrealizable core computations. We evaluate the presented heuristics on SYNTECH15, a total of 78 specifications of 6 autonomous Lego robots, written by 3rd year undergraduate computer science students in a project class we have taught, as well as on several benchmarks from the literature. The evaluation investigates not only the potential of the suggested heuristics to improve computation times, but also the difference between existing benchmarks and the robot's specifications in terms of the effectiveness of the heuristics.

cs.LO

Symbolic BDD and ADD Algorithms for Energy Games

Energy games, which model quantitative consumption of a limited resource, e.g., time or energy, play a central role in quantitative models for reactive systems. Reactive synthesis constructs a controller which satisfies a given specification, if one exists. For energy games a synthesized controller ensures to satisfy not only the safety constraints of the specification but also the quantitative constraints expressed in the energy game. A symbolic algorithm for energy games, recently presented by Chatterjee et al., is symbolic in its representation of quantitative values but concrete in the representation of game states and transitions. In this paper we present an algorithm that is symbolic both in the quantitative values and in the underlying game representation. We have implemented our algorithm using two different symbolic representations for reactive games, Binary Decision Diagrams (BDD) and Algebraic Decision Diagrams (ADD). We investigate the commonalities and differences of the two implementations and compare their running times on specifications of energy games.

cs.LO

Synthesizing a Lego Forklift Controller in GR(1): A Case Study

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from a given specification. GR(1) is a well-known fragment of linear temporal logic (LTL) where synthesis is possible using a polynomial symbolic algorithm. We conducted a case study to learn about the challenges that software engineers may face when using GR(1) synthesis for the development of a reactive robotic system. In the case study we developed two variants of a forklift controller, deployed on a Lego robot. The case study employs LTL specification patterns as an extension of the GR(1) specification language, an examination of two specification variants for execution scheduling, traceability from the synthesized controller to constraints in the specification, and generated counter strategies to support understanding reasons for unrealizability. We present the specifications we developed, our observations, and challenges faced during the case study.

cs.SE

Behavioral Compatibility of Simulink Models for Product Line Maintenance and Evolution

Embedded software systems, e.g. automotive, robotic or automation systems are highly configurable and consist of many software components being available in different variants and versions. To identify the degree of reusability between these different occurrences of a component, it is necessary to determine the functional backward and forward compatibility between them. Based on this information it is possible to identify in which system context a component can be replaced safely by another version, e.g. exchanging an older component, or variant, e.g. introducing new features, to achieve the same functionality. This paper presents a model checking approach to determine behavioral compatibility of Simulink models, obtained from different component variants or during evolution. A prototype for automated compatibility checking demonstrates its feasibility. In addition implemented optimizations make the analysis more efficient, when the compared variants or versions are structurally similar. A case study on a driver assistance system provided by Daimler AG shows the effectiveness of the approach to automatically compare Simulink components.

cs.SE

Architecture and Behavior Modeling of Cyber-Physical Systems with MontiArcAutomaton

This book presents MontiArcAutomaton, a modeling language for architecture and be- havior modeling of Cyber-Physical Systems as interactive Component & Connector mod- els. MontiArcAutomaton extends the Architecture Description Language MontiArc with automata to describe component behavior. The modeling language MontiArcAutomaton provides syntactical elements for defin- ing automata with states, variables, and transitions inside MontiArc components. These syntactical elements and a basic set of well-formedness rules provide the syntax for a fam- ily of modeling languages for state-based behavior modeling in Component & Connector architectures. We present two concrete language profiles with additional well-formedness rules to model time-synchronous component behavior and untimed, event-driven behav- ior of components. This book gives an overview of the MontiArcAutomaton language including examples, a language reference, and a context-free grammar for MontiArcAutomaton models. It also provides syntax definition, well-formedness rules, and semantics for two language profiles. We summarize projects and case studies applying MontiArcAutomaton. MontiArcAutomaton is implemented using the DSL framework MontiCore. Available tools include a textual editor with syntax highlighting and code completion as well as a graphical editor and a powerful and extensible code generation framework for target languages including EMF, Java, Mona, and Python.

cs.SE

Code Generator Composition for Model-Driven Engineering of Robotics Component & Connector Systems

Engineering software for robotics applications requires multidomain and application-specific solutions. Model-driven engineering and modeling language integration provide means for developing specialized, yet reusable models of robotics software architectures. Code generators transform these platform independent models into executable code specific to robotic platforms. Generative software engineering for multidomain applications requires not only the integration of modeling languages but also the integration of validation mechanisms and code generators. In this paper we sketch a conceptual model for code generator composition and show an instantiation of this model in the MontiArc- Automaton framework. MontiArcAutomaton allows modeling software architectures as component and connector models with different component behavior modeling languages. Effective means for code generator integration are a necessity for the post hoc integration of applicationspecific languages in model-based robotics software engineering.

cs.SE

Multi-Platform Generative Development of Component & Connector Systems using Model and Code Libraries

Component-based software engineering aims to reduce software development effort by reusing established components as building blocks of complex systems. Defining components in general-purpose programming languages restricts their reuse to platforms supporting these languages and complicates component composition with implementation details. The vision of model-driven engineering is to reduce the gap between developer intention and implementation details by lifting abstract models to primary development artifacts and systematically transforming these into executable systems. For sufficiently complex systems the transformation from abstract models to platform-specific implementations requires augmentation with platform-specific components. We propose a model-driven mechanism to transform platform-independent logical component & connector architectures into platform-specific implementations combining model and code libraries. This mechanism allows to postpone commitment to a specific platform and thus increases reuse of software architectures and components.

cs.SE

MontiArc - Architectural Modeling of Interactive Distributed and Cyber-Physical Systems

This report presents MontiArc, a modeling language for the description of Component & Connector architectures. A component is a unit executing computations and/or storing data. Information flow between components is modeled via unidirectional connectors connecting typed, directed ports of the interfaces of components. Language features of the ADL MontiArc include hierarchical decomposition of components, subtyping by structural inheritance, component type definitions and reference declarations for reuse, generic component types and configurable components, syntactic sugar for connectors, and controlled implicit creation of connections and subcomponent declarations. This technical report gives an overview of the MontiArc language and is a reference for the MontiArc grammar intended to enable reuse and extension of MontiArc and MontiArc related tools. MontiArc is implemented using the DSL framework MontiCore. Available tools include an editor with syntax highlighting and code completion as well as a simulation framework with a Java code generator.

cs.SE

System Model-Based Definition of Modeling Language Semantics

In this paper, we present an approach to define the semantics for object-oriented modeling languages. One important property of this semantics is to support underspecified and incomplete models. To this end, semantics is given as predicates over elements of the semantic domain. This domain is called the system model which is a general declarative characterization of object systems. The system model is very detailed since it captures various relevant structural, behavioral, and interaction aspects. This allows us to re-use the system model as a domain for various kinds of object-oriented modeling languages. As a major consequence the integration of language semantics is straight-forward. The whole approach is supported by tools that do not constrain the semantics definition's expressiveness and flexibility while making it machinecheckable.

cs.SE

Summarizing Semantic Model Differences

Fundamental building blocks for managing and understanding software evolution in the context of model-driven engineering are differencing operators one can use for model comparisons. Semantic model differencing deals with the definition and computation of semantic diff operators for model comparison, operators whose input consists of two models and whose output is a set of diff witnesses, instances of one model that are not instances of the other. However, in many cases the complete set of diff witnesses is too large to be efficiently computed and effectively presented. Moreover, many of the witnesses are very similar and hence not interesting. Thus, an important challenge of semantic differencing relates to witness selection and presentation. In this paper we propose to address this challenge using a summarization technique, based on a notion of equivalence that partitions the set of diff witnesses. The result of the computation is a summary set, consisting of a single representative witness from each equivalence class. We demonstrate our ideas using two concrete diff operators, for class diagrams and for activity diagrams, where the computation of the summary set is efficient and does not require the enumeration of all witnesses.

cs.SE

MontiArcAutomaton: Modeling Architecture and Behavior of Robotic Systems

Robotics poses a challenge for software engineering as the vast numbers of different robot platforms impose different requirements on robot control architectures. The platform dependent development of robotic applications impedes reusability and portability. The lack of reusability hampers broad propagation of robotics applications. The MontiArcAutomaton architecture and behavior modeling framework provides an integrated, platform independent structure and behavior modeling language with an extensible code generation framework. MontiArcAutomaton's central concept is encapsulation and decomposition known from Component & Connector Architecture Description Languages. This concept is extended from the modeling language to the code generation and target runtime framework to bridge the gap of platform specific and independent implementations along well designed interfaces. This facilitates the reuse of robot applications and makes their development more efficient.

cs.SE

Semantically Configurable Consistency Analysis for Class and Object Diagrams

Checking consistency between an object diagram (OD) and a class diagram (CD) is an important analysis problem. However, several variations in the semantics of CDs and ODs, as used in different contexts and for different purposes, create a challenge for analysis tools. To address this challenge in this paper we investigate semantically configurable model analysis. We formalize the variability in the languages semantics using a feature model: each configuration that the model permits induces a different semantics. Moreover, we develop a parametrized analysis that can be instantiated to comply with every legal configuration of the feature model. Thus, the analysis is semantically congured and its results change according to the semantics induced by the selected feature configuration. The ideas are implemented using a parametrized transformation to Alloy. The work can be viewed as a case study example for a formal and automated approach to handling semantic variability in modeling languages.

cs.SE

CD2Alloy: Class Diagrams Analysis Using Alloy Revisited

We present CD2Alloy, a novel, powerful translation of UML class diagrams (CDs) to Alloy. Unlike existing translations, which are based on a shallow embedding strategy, and are thus limited to checking consistency and generating conforming object models of a single CD, and support a limited set of CD language features, CD2Alloy uses a deeper embedding strategy. Rather than mapping each CD construct to a semantically equivalent Alloy construct, CD2Alloy defines (some) CD constructs as new concepts within Alloy. This enables solving several analysis problems that involve more than one CD and could not be solved by earlier works, and supporting an extended list of CD language features. The ideas are implemented in a prototype Eclipse plug-in. The work advances the state-of-the-art in CD analysis, and can also be viewed as an interesting case study for the different possible translations of one modeling language to another, their strengths and weaknesses.

cs.SE

ADDiff: Semantic Differencing for Activity Diagrams

Activity diagrams (ADs) have recently become widely used in the modeling of workflows, business processes, and web-services, where they serve various purposes, from documentation, requirement definitions, and test case specifications, to simulation and code generation. As models, programs, and systems evolve over time, understanding changes and their impact is an important challenge, which has attracted much research efforts in recent years. In this paper we present addiff, a semantic differencing operator for ADs. Unlike most existing approaches to model comparison, which compare the concrete or the abstract syntax of two given diagrams and output a list of syntactical changes or edit operations, addiff considers the Semantics of the diagrams at hand and outputs a set of diff witnesses, each of which is an execution trace that is possible in the first AD and is not possible in the second. We motivate the use of addiff, formally define it, and show two algorithms to compute it, a concrete forward-search algorithm and a symbolic xpoint algorithm, implemented using BDDs and integrated into the Eclipse IDE. Empirical results and examples demonstrate the feasibility and unique contribution of addiff to the state-of-the-art in version comparison and evolution analysis.

cs.SE