Showing 1–31 of 31 results for author: Rueß, H

Efficient Reactive Synthesis

Authors: Xin Ye, Harald Ruess

Abstract: Our main result is a polynomial time algorithm for deciding realizability for the GXU sublogic of linear temporal logic. This logic is particularly suitable for the specification of embedded control systems, and it is more expressive than GR(1). Reactive control programs for GXU specifications are represented as Mealy machines, which are extended by the monitoring of input events. Now, realizabili… ▽ More Our main result is a polynomial time algorithm for deciding realizability for the GXU sublogic of linear temporal logic. This logic is particularly suitable for the specification of embedded control systems, and it is more expressive than GR(1). Reactive control programs for GXU specifications are represented as Mealy machines, which are extended by the monitoring of input events. Now, realizability for GXU specifications is shown to be equivalent to solving a certain subclass of 2QBF satisfiability problems. These logical problems can be solved in cubic time in the size of GXU specifications. For unrealizable GXU specifications, stronger environment assumptions are mined from failed consistency checks based on Padoa's characterization of definability and Craig interpolation. △ Less

Submitted 27 April, 2024; originally announced April 2024.

Formal Specification, Assessment, and Enforcement of Fairness for Generative AIs

Authors: Chih-Hong Cheng, Changshun Wu, Harald Ruess, Xingyu Zhao, Saddek Bensalem

Abstract: Reinforcing or even exacerbating societal biases and inequalities will increase significantly as generative AI increasingly produces useful artifacts, from text to images and beyond, for the real world. We address these issues by formally characterizing the notion of fairness for generative AI as a basis for monitoring and enforcing fairness. We define two levels of fairness using the notion of in… ▽ More Reinforcing or even exacerbating societal biases and inequalities will increase significantly as generative AI increasingly produces useful artifacts, from text to images and beyond, for the real world. We address these issues by formally characterizing the notion of fairness for generative AI as a basis for monitoring and enforcing fairness. We define two levels of fairness using the notion of infinite sequences of abstractions of AI-generated artifacts such as text or images. The first is the fairness demonstrated on the generated sequences, which is evaluated only on the outputs while agnostic to the prompts and models used. The second is the inherent fairness of the generative AI model, which requires that fairness be manifested when input prompts are neutral, that is, they do not explicitly instruct the generative AI to produce a particular type of output. We also study relative intersectional fairness to counteract the combinatorial explosion of fairness when considering multiple categories together with lazy fairness enforcement. Finally, fairness monitoring and enforcement are tested against some current generative AI models. △ Less

Submitted 6 May, 2024; v1 submitted 25 April, 2024; originally announced April 2024.

A Decision Method for Elementary Stream Calculus

Authors: Harald Ruess

Abstract: The main result is a doubly exponential decision procedure for the first-order equality theory of streams with both arithmetic and control-oriented stream operations. This stream logic is expressive for elementary problems of stream calculus. The main result is a doubly exponential decision procedure for the first-order equality theory of streams with both arithmetic and control-oriented stream operations. This stream logic is expressive for elementary problems of stream calculus. △ Less

Submitted 4 January, 2024; originally announced January 2024.

Comments: 19 pages

MSC Class: I.1; J.6; F.4

Solving Causal Stream Inclusions

Authors: Harald Ruess

Abstract: We study solutions to systems of stream inclusions of the form 'f in T(f)', where the nondeterministic transformer 'T' on omega-infinite streams is assumed to be causal in the sense that elements in output streams are determined by a finite prefix of inputs. We first establish a correspondence between logic-based causality and metric-based contraction. Based on this causality-contraction connectio… ▽ More We study solutions to systems of stream inclusions of the form 'f in T(f)', where the nondeterministic transformer 'T' on omega-infinite streams is assumed to be causal in the sense that elements in output streams are determined by a finite prefix of inputs. We first establish a correspondence between logic-based causality and metric-based contraction. Based on this causality-contraction connection we then apply fixpoint principles to the spherically complete ultrametric space of streams to construct solutions of stream inclusions. The underlying fixpoint iterations induce fixpoint induction principles to reason about these solutions.In addition, the fixpoint approximation provides an anytime algorithm with which finite prefixes of solutions can be calculated. These developments are illustrated for some central concepts of system design. △ Less

Submitted 24 June, 2024; v1 submitted 30 December, 2023; originally announced January 2024.

MSC Class: D.2; F.2

Safety Performance of Neural Networks in the Presence of Covariate Shift

Authors: Chih-Hong Cheng, Harald Ruess, Konstantinos Theodorou

Abstract: Covariate shift may impact the operational safety performance of neural networks. A re-evaluation of the safety performance, however, requires collecting new operational data and creating corresponding ground truth labels, which often is not possible during operation. We are therefore proposing to reshape the initial test set, as used for the safety performance evaluation prior to deployment, base… ▽ More Covariate shift may impact the operational safety performance of neural networks. A re-evaluation of the safety performance, however, requires collecting new operational data and creating corresponding ground truth labels, which often is not possible during operation. We are therefore proposing to reshape the initial test set, as used for the safety performance evaluation prior to deployment, based on an approximation of the operational data. This approximation is obtained by observing and learning the distribution of activation patterns of neurons in the network during operation. The reshaped test set reflects the distribution of neuron activation values as observed during operation, and may therefore be used for re-evaluating safety performance in the presence of covariate shift. First, we derive conservative bounds on the values of neurons by applying finite binning and static dataflow analysis. Second, we formulate a mixed integer linear programming (MILP) constraint for constructing the minimum set of data points to be removed in the test set, such that the difference between the discretized test and operational distributions is bounded. We discuss potential benefits and limitations of this constraint-based approach based on our initial experience with an implemented research prototype. △ Less

Submitted 24 July, 2023; originally announced July 2023.

Towards Rigorous Design of OoD Detectors

Authors: Chih-Hong Cheng, Changshun Wu, Harald Ruess, Saddek Bensalem

Abstract: Out-of-distribution (OoD) detection techniques are instrumental for safety-related neural networks. We are arguing, however, that current performance-oriented OoD detection techniques geared towards matching metrics such as expected calibration error, are not sufficient for establishing safety claims. What is missing is a rigorous design approach for develo**, verifying, and validating OoD detec… ▽ More Out-of-distribution (OoD) detection techniques are instrumental for safety-related neural networks. We are arguing, however, that current performance-oriented OoD detection techniques geared towards matching metrics such as expected calibration error, are not sufficient for establishing safety claims. What is missing is a rigorous design approach for develo**, verifying, and validating OoD detectors. These design principles need to be aligned with the intended functionality and the operational domain. Here, we formulate some of the key technical challenges, together with a possible way forward, for develo** a rigorous and safety-related design methodology for OoD detectors. △ Less

Submitted 14 June, 2023; originally announced June 2023.

Evidential Transactions with Cyberlogic

Authors: Harald Ruess, Natarajan Shankar

Abstract: Cyberlogic is an enabling logical foundation for building and analyzing digital transactions that involve the exchange of digital forms of evidence. It is based on an extension of (first-order) intuitionistic predicate logic with an attestation and a knowledge modality. The key ideas underlying Cyberlogic are extremely simple, as (1) public keys correspond to authorizations, (2) transactions are s… ▽ More Cyberlogic is an enabling logical foundation for building and analyzing digital transactions that involve the exchange of digital forms of evidence. It is based on an extension of (first-order) intuitionistic predicate logic with an attestation and a knowledge modality. The key ideas underlying Cyberlogic are extremely simple, as (1) public keys correspond to authorizations, (2) transactions are specified as distributed logic programs, and (3) verifiable evidence is collected by means of distributed proof search. Verifiable evidence, in particular, are constructed from extra-logical elements such as signed documents and cryptographic signatures. Despite this conceptual simplicity of Cyberlogic, central features of authorization policies including trust, delegation, and revocation of authority are definable. An expressive temporal-epistemic logic for specifying distributed authorization policies and protocols is therefore definable in Cyberlogic using a trusted time source. We describe the distributed execution of Cyberlogic programs based on the hereditary Harrop fragment in terms of distributed proof search, and we illustrate some fundamental issues in the distributed construction of certificates. The main principles of encoding and executing cryptographic protocols in Cyberlogic are demonstrated. Finally, a functional encryption scheme is proposed for checking certificates of evidential transactions when policies are kept private. △ Less

Submitted 20 March, 2023; originally announced April 2023.

Comments: 41 pages

Report number: SRI International, CSL Technical Report SRI-CSL-2023-01 MSC Class: 68M11

Safe AI -- How is this Possible?

Authors: Harald Rueß, Simon Burton

Abstract: Ttraditional safety engineering is coming to a turning point moving from deterministic, non-evolving systems operating in well-defined contexts to increasingly autonomous and learning-enabled AI systems which are acting in largely unpredictable operating contexts. We outline some of underlying challenges of safe AI and suggest a rigorous engineering framework for minimizing uncertainty, thereby in… ▽ More Ttraditional safety engineering is coming to a turning point moving from deterministic, non-evolving systems operating in well-defined contexts to increasingly autonomous and learning-enabled AI systems which are acting in largely unpredictable operating contexts. We outline some of underlying challenges of safe AI and suggest a rigorous engineering framework for minimizing uncertainty, thereby increasing confidence, up to tolerable levels, in the safe behavior of AI systems. △ Less

Submitted 11 May, 2022; v1 submitted 25 January, 2022; originally announced January 2022.

Comments: 42 pages, 4 figures, 1 table

Systems Challenges for Trustworthy Embodied Systems

Authors: Harald Rueß

Abstract: A new generation of increasingly autonomous and self-learning embodied systems is about to be developed. When deploying embodied systems into a real-life context we face various engineering challenges, as it is crucial to coordinate the behavior of embodied systems in a beneficial manner, ensure their compatibility with our human-centered social values, and design verifiably safe and reliable huma… ▽ More A new generation of increasingly autonomous and self-learning embodied systems is about to be developed. When deploying embodied systems into a real-life context we face various engineering challenges, as it is crucial to coordinate the behavior of embodied systems in a beneficial manner, ensure their compatibility with our human-centered social values, and design verifiably safe and reliable human-machine interaction. We are arguing that traditional systems engineering is coming to a climacteric from embedded to embodied systems, and with assuring the trustworthiness of dynamic federations of situationally aware, intent-driven, explorative, ever-evolving, largely non-predictable, and increasingly autonomous embodied systems in uncertain, complex, and unpredictable real-world contexts. We are therefore identifying a number of urgent systems challenges for trustworthy embodied systems, including robust and human-centric AI, cognitive architectures, uncertainty quantification, trustworthy self-integration, and continual analysis and assurance. △ Less

Submitted 26 April, 2022; v1 submitted 10 January, 2022; originally announced January 2022.

Comments: 57 pages, 7 figures, 3 tables. Public project deliverable, fortiss whitepaper

Security Engineering for ISO 21434

Authors: Yuri Gil Dantas, Vivek Nigam, Harald Ruess

Abstract: The ISO 21434 is a new standard that has been proposed to address the future challenges of automotive cybersecurity. This white paper takes a closer look at the ISO 21434 hel** engineers to understand the ISO 21434 parts, the key activities to be carried out and the main artefacts that shall be produced. As any certification, obtaining the ISO 21434 certification can be daunting at first sight.… ▽ More The ISO 21434 is a new standard that has been proposed to address the future challenges of automotive cybersecurity. This white paper takes a closer look at the ISO 21434 hel** engineers to understand the ISO 21434 parts, the key activities to be carried out and the main artefacts that shall be produced. As any certification, obtaining the ISO 21434 certification can be daunting at first sight. Engineers have to deploy processes that include several security risk assessment methods to produce security arguments and evidence supporting item security claims. In this white paper, we propose a security engineering approach that can ease this process by relying on Rigorous Security Assessments and Incremental Assessment Maintenance methods supported by automation. We demonstrate by example that the proposed approach can greatly increase the quality of the produced artefacts, the efficiency to produce them, as well as enable continuous security assessment. Finally, we point out some key research directions that we are investigating to fully realize the proposed approach. △ Less

Submitted 17 January, 2021; v1 submitted 30 December, 2020; originally announced December 2020.

Comments: This is a White Paper. This is a preliminary version. Its figures and template are to be finalized by our marketing department. V3 corrects a number of typos

ACM Class: I.2.4; I.2.5

Knowledge as Invariance -- History and Perspectives of Knowledge-augmented Machine Learning

Authors: Alexander Sagel, Amit Sahu, Stefan Matthes, Holger Pfeifer, Tianming Qiu, Harald Rueß, Hao Shen, Julian Wörmann

Abstract: Research in machine learning is at a turning point. While supervised deep learning has conquered the field at a breathtaking pace and demonstrated the ability to solve inference problems with unprecedented accuracy, it still does not quite live up to its name if we think of learning as the process of acquiring knowledge about a subject or problem. Major weaknesses of present-day deep learning mode… ▽ More Research in machine learning is at a turning point. While supervised deep learning has conquered the field at a breathtaking pace and demonstrated the ability to solve inference problems with unprecedented accuracy, it still does not quite live up to its name if we think of learning as the process of acquiring knowledge about a subject or problem. Major weaknesses of present-day deep learning models are, for instance, their lack of adaptability to changes of environment or their incapability to perform other kinds of tasks than the one they were trained for. While it is still unclear how to overcome these limitations, one can observe a paradigm shift within the machine learning community, with research interests shifting away from increasing the performance of highly parameterized models to exceedingly specific tasks, and towards employing machine learning algorithms in highly diverse domains. This research question can be approached from different angles. For instance, the field of Informed AI investigates the problem of infusing domain knowledge into a machine learning model, by using techniques such as regularization, data augmentation or post-processing. On the other hand, a remarkable number of works in the recent years has focused on develo** models that by themselves guarantee a certain degree of versatility and invariance with respect to the domain or problem at hand. Thus, rather than investigating how to provide domain-specific knowledge to machine learning models, these works explore methods that equip the models with the capability of acquiring the knowledge by themselves. This white paper provides an introduction and discussion of this emerging field in machine learning research. To this end, it reviews the role of knowledge in machine learning, and discusses its relation to the concept of invariance, before providing a literature review of the field. △ Less

Submitted 21 December, 2020; originally announced December 2020.

Model-Based Safety and Security Engineering

Authors: Vivek Nigam, Alexander Pretschner, Harald Ruess

Abstract: By exploiting the increasing surface attack of systems, cyber-attacks can cause catastrophic events, such as, remotely disable safety mechanisms. This means that in order to avoid hazards, safety and security need to be integrated, exchanging information, such as, key hazards/threats, risk evaluations, mechanisms used. This white paper describes some steps towards this integration by using models.… ▽ More By exploiting the increasing surface attack of systems, cyber-attacks can cause catastrophic events, such as, remotely disable safety mechanisms. This means that in order to avoid hazards, safety and security need to be integrated, exchanging information, such as, key hazards/threats, risk evaluations, mechanisms used. This white paper describes some steps towards this integration by using models. We start by identifying some key technical challenges. Then we demonstrate how models, such as Goal Structured Notation (GSN) for safety and Attack Defense Trees (ADT) for security, can address these challenges. In particular, (1) we demonstrate how to extract in an automated fashion security relevant information from safety assessments by translating GSN-Models into ADTs; (2) We show how security results can impact the confidence of safety assessments; (3) We propose a collaborative development process where safety and security assessments are built by incrementally taking into account safety and security analysis; (4) We describe how to carry out trade-off analysis in an automated fashion, such as identifying when safety and security arguments contradict each other and how to solve such contradictions. We conclude pointing out that these are the first steps towards a wide range of techniques to support Safety and Security Engineering. As a white paper, we avoid being too technical, preferring to illustrate features by using examples and thus being more accessible. △ Less

Submitted 2 January, 2019; v1 submitted 11 October, 2018; originally announced October 2018.

Comments: White paper on Safety and Security Engineering using Models

Towards Dependability Metrics for Neural Networks

Authors: Chih-Hong Cheng, Georg Nührenberg, Chung-Hao Huang, Harald Ruess, Hirotoshi Yasuoka

Abstract: Artificial neural networks (NN) are instrumental in realizing highly-automated driving functionality. An overarching challenge is to identify best safety engineering practices for NN and other learning-enabled components. In particular, there is an urgent need for an adequate set of metrics for measuring all-important NN dependability attributes. We address this challenge by proposing a number of… ▽ More Artificial neural networks (NN) are instrumental in realizing highly-automated driving functionality. An overarching challenge is to identify best safety engineering practices for NN and other learning-enabled components. In particular, there is an urgent need for an adequate set of metrics for measuring all-important NN dependability attributes. We address this challenge by proposing a number of NN-specific and efficiently computable metrics for measuring NN dependability attributes including robustness, interpretability, completeness, and correctness. △ Less

Submitted 8 June, 2018; v1 submitted 6 June, 2018; originally announced June 2018.

Verification of Binarized Neural Networks via Inter-Neuron Factoring

Authors: Chih-Hong Cheng, Georg Nührenberg, Chung-Hao Huang, Harald Ruess

Abstract: We study the problem of formal verification of Binarized Neural Networks (BNN), which have recently been proposed as a energy-efficient alternative to traditional learning networks. The verification of BNNs, using the reduction to hardware verification, can be even more scalable by factoring computations among neurons within the same layer. By proving the NP-hardness of finding optimal factoring a… ▽ More We study the problem of formal verification of Binarized Neural Networks (BNN), which have recently been proposed as a energy-efficient alternative to traditional learning networks. The verification of BNNs, using the reduction to hardware verification, can be even more scalable by factoring computations among neurons within the same layer. By proving the NP-hardness of finding optimal factoring as well as the hardness of PTAS approximability, we design polynomial-time search heuristics to generate factoring solutions. The overall framework allows applying verification techniques to moderately-sized BNNs for embedded devices with thousands of neurons and inputs. △ Less

Submitted 19 January, 2018; v1 submitted 9 October, 2017; originally announced October 2017.

Comments: Version 2: add proofs for hardness of PTAS approximability, remove experiments on randomized examples and some not-so-important optimizations

Neural Networks for Safety-Critical Applications - Challenges, Experiments and Perspectives

Authors: Chih-Hong Cheng, Frederik Diehl, Yassine Hamza, Gereon Hinz, Georg Nührenberg, Markus Rickert, Harald Ruess, Michael Troung-Le

Abstract: We propose a methodology for designing dependable Artificial Neural Networks (ANN) by extending the concepts of understandability, correctness, and validity that are crucial ingredients in existing certification standards. We apply the concept in a concrete case study in designing a high-way ANN-based motion predictor to guarantee safety properties such as impossibility for the ego vehicle to sugg… ▽ More We propose a methodology for designing dependable Artificial Neural Networks (ANN) by extending the concepts of understandability, correctness, and validity that are crucial ingredients in existing certification standards. We apply the concept in a concrete case study in designing a high-way ANN-based motion predictor to guarantee safety properties such as impossibility for the ego vehicle to suggest moving to the right lane if there exists another vehicle on its right. △ Less

Submitted 4 September, 2017; originally announced September 2017.

Comments: Summary for activities conducted in the fortiss Eigenforschungsprojekt "TdpSW - Towards dependable and predictable SW for ML-based autonomous systems". All ANN-based motion predictors being formally analyzed are available in the source file

Maximum Resilience of Artificial Neural Networks

Authors: Chih-Hong Cheng, Georg Nührenberg, Harald Ruess

Abstract: The deployment of Artificial Neural Networks (ANNs) in safety-critical applications poses a number of new verification and certification challenges. In particular, for ANN-enabled self-driving vehicles it is important to establish properties about the resilience of ANNs to noisy or even maliciously manipulated sensory input. We are addressing these challenges by defining resilience properties of A… ▽ More The deployment of Artificial Neural Networks (ANNs) in safety-critical applications poses a number of new verification and certification challenges. In particular, for ANN-enabled self-driving vehicles it is important to establish properties about the resilience of ANNs to noisy or even maliciously manipulated sensory input. We are addressing these challenges by defining resilience properties of ANN-based classifiers as the maximal amount of input or sensor perturbation which is still tolerated. This problem of computing maximal perturbation bounds for ANNs is then reduced to solving mixed integer optimization problems (MIP). A number of MIP encoding heuristics are developed for drastically reducing MIP-solver runtimes, and using parallelization of MIP-solvers results in an almost linear speed-up in the number (up to a certain limit) of computing cores in our experiments. We demonstrate the effectiveness and scalability of our approach by means of computing maximal resilience bounds for a number of ANN benchmark sets ranging from typical image recognition scenarios to the autonomous maneuvering of robots. △ Less

Submitted 5 July, 2017; v1 submitted 28 April, 2017; originally announced May 2017.

Comments: Timestamp research work conducted in the project. version 2: fix some typos, rephrase the definition, and add some more existing work

Automated Analysis of Multi-View Software Architectures

Authors: Chih-Hong Cheng, Yassine Hamza, Harald Ruess

Abstract: Software architectures usually are comprised of different views for capturing static, runtime, and deployment aspects. What is currently missing, however, are formal validation and verification techniques of multi-view architecture in very early phases of the software development lifecycle. The main contribution of this paper therefore is the construction of a single formal model (in Promela) for… ▽ More Software architectures usually are comprised of different views for capturing static, runtime, and deployment aspects. What is currently missing, however, are formal validation and verification techniques of multi-view architecture in very early phases of the software development lifecycle. The main contribution of this paper therefore is the construction of a single formal model (in Promela) for certain stylized, and widely used, multi-view architectures by suitably interpreting and fusing sub-models from different UML diagrams. Possible counter-examples produced by model checking are fed back as test scenarios for debugging the multi-view architectural model. We have implemented this algorithm as a plug-in for the Enterprise Architect development tool, and successfully used SPIN model checking for debugging some industrial architectural multi-view models by identifying a number of undesirable corner cases. △ Less

Submitted 24 April, 2017; originally announced April 2017.

Comments: Timestam** research work conducted under the fortiss Eigenforschung project

Structural Synthesis for GXW Specifications

Authors: Chih-Hong Cheng, Yassine Hamza, Harald Ruess

Abstract: We define the GXW fragment of linear temporal logic (LTL) as the basis for synthesizing embedded control software for safety-critical applications. Since GXW includes the use of a weak-until operator we are able to specify a number of diverse programmable logic control (PLC) problems, which we have compiled from industrial training sets. For GXW controller specifications, we develop a novel approa… ▽ More We define the GXW fragment of linear temporal logic (LTL) as the basis for synthesizing embedded control software for safety-critical applications. Since GXW includes the use of a weak-until operator we are able to specify a number of diverse programmable logic control (PLC) problems, which we have compiled from industrial training sets. For GXW controller specifications, we develop a novel approach for synthesizing a set of synchronously communicating actor-based controllers. This synthesis algorithm proceeds by means of recursing over the structure of GXW specifications, and generates a set of dedicated and synchronously communicating sub-controllers according to the formula structure. In a subsequent step, 2QBF constraint solving identifies and tries to resolve potential conflicts between individual GXW specifications. This structural approach to GXW synthesis supports traceability between requirements and the generated control code as mandated by certification regimes for safety-critical software. Synthesis for GXW specifications is in PSPACE compared to 2EXPTIME-completeness of full-fledged LTL synthesis. Indeed our experimental results suggest that GXW synthesis scales well to industrial-sized control synthesis problems with 20 input and output ports and beyond. △ Less

Submitted 6 July, 2016; v1 submitted 4 May, 2016; originally announced May 2016.

Comments: The long (including appendix) version being reviewed by CAV'16 program committee. Compared to the submitted version, one author (out of her wish) is moved to the Acknowledgement. (v2) Corrected typos. (v3) Add an additional remark over environment assumption and easy corner cases

Time-resolved magnetophotoluminescence studies of magnetic polaron dynamics in type-II quantum dots

Authors: B. Barman, R. Oszwałdowski, L. Schweidenback, A. H. Russ, J. M. Pientka, Y. Tsai, W-C. Chou, W. C. Fan, J. R. Murphy, A. N. Cartwright, I. R. Sellers, A. G. Petukhov, I. Žutić, B. D. McCombe, A. Petrou

Abstract: We used continuous wave photoluminescence (cw-PL) and time resolved photoluminescence (TR-PL) spectroscopy to compare the properties of magnetic polarons (MP) in two related spatially indirect II-VI epitaxially grown quantum dot systems. In the ZnTe/(Zn,Mn)Se system the holes are confined in the non-magnetic ZnTe quantum dots (QDs), and the electrons reside in the magnetic (Zn,Mn)Se matrix. On the… ▽ More We used continuous wave photoluminescence (cw-PL) and time resolved photoluminescence (TR-PL) spectroscopy to compare the properties of magnetic polarons (MP) in two related spatially indirect II-VI epitaxially grown quantum dot systems. In the ZnTe/(Zn,Mn)Se system the holes are confined in the non-magnetic ZnTe quantum dots (QDs), and the electrons reside in the magnetic (Zn,Mn)Se matrix. On the other hand, in the (Zn,Mn)Te/ZnSe system, the holes are confined in the magnetic (Zn,Mn)Te QDs, while the electrons remain in the surrounding non-magnetic ZnSe matrix. The magnetic polaron formation energies in both systems were measured from the temporal red-shift of the band-edge emission. The magnetic polaron exhibits distinct characteristics depending on the location of the Mn ions. In the ZnTe/(Zn,Mn)Se system the magnetic polaron shows conventional behavior with decreasing with increasing temperature T and increasing magnetic field B. In contrast, in the (Zn,Mn)Te/ZnSe system has unconventional dependence on temperature T and magnetic field B; is weakly dependent on T as well as on B. We discuss a possible origin for such a striking difference in the MP properties in two closely related QD systems. △ Less

Submitted 14 October, 2015; originally announced October 2015.

Comments: 27 pages, 12 figures

Journal ref: PhysRevB.92.035430(2015)

Timed Orchestration for Component-based Systems

Authors: Chih-Hong Cheng, Lacramioara Astefanoaei, Harald Ruess, Souha Ben Rayana, Saddek Bensalem

Abstract: Individual machines in flexible production lines explicitly expose capabilities at their interfaces by means of parametric skills. Given such a set of configurable machines, a line integrator is faced with the problem of finding and tuning parameters for each machine such that the overall production line implements given safety and temporal requirements in an optimized and robust fashion. We forma… ▽ More Individual machines in flexible production lines explicitly expose capabilities at their interfaces by means of parametric skills. Given such a set of configurable machines, a line integrator is faced with the problem of finding and tuning parameters for each machine such that the overall production line implements given safety and temporal requirements in an optimized and robust fashion. We formalize this problem of configuring and orchestrating flexible production lines as a parameter synthesis problem for systems of parametric timed automata, where interactions are based on skills. Parameter synthesis problems for interaction-level LTL properties are translated to parameter synthesis problems for state-based safety properties. For safety properties, synthesis problems are solved by checking satisfiability of $\exists\forall$SMT constraints. For constraint generation, we provide a set of computationally cheap over-approximations of the set of reachable states, together with fence constructions as sufficient conditions for safety formulas. We demonstrate the feasibility of our approach by solving typical machine configuration problems as encountered in industrial automation. △ Less

Submitted 20 May, 2016; v1 submitted 21 April, 2015; originally announced April 2015.

Comments: Timestamp of the work, with evaluation added by creating MES orchestration examples. (v3): typo fix and bring back definition and citation in en^t as in v1

G4LTL-ST: Automatic Generation of PLC Programs

Authors: Chih-Hong Cheng, Chung-Hao Huang, Harald Ruess, Stefan Stattelmann

Abstract: G4LTL-ST automatically synthesizes control code for industrial Programmable Logic Controls (PLC) from timed behavioral specifications of input-output signals. These specifications are expressed in a linear temporal logic (LTL) extended with non-linear arithmetic constraints and timing constraints on signals. G4LTL-ST generates code in IEC 61131-3-compatible Structured Text, which is compiled into… ▽ More G4LTL-ST automatically synthesizes control code for industrial Programmable Logic Controls (PLC) from timed behavioral specifications of input-output signals. These specifications are expressed in a linear temporal logic (LTL) extended with non-linear arithmetic constraints and timing constraints on signals. G4LTL-ST generates code in IEC 61131-3-compatible Structured Text, which is compiled into executable code for a large number of industrial field-level devices. The synthesis algorithm of G4LTL-ST implements pseudo-Boolean abstraction of data constraints and the compilation of timing constraints into LTL, together with a counterstrategy-guided abstraction refinement synthesis loop. Since temporal logic specifications are notoriously difficult to use in practice, G4LTL-ST supports engineers in specifying realizable control problems by suggesting suitable restrictions on the behavior of the control environment from failed synthesis attempts. △ Less

Submitted 15 May, 2014; v1 submitted 10 May, 2014; originally announced May 2014.

Comments: This is the full version of the CAV'14 paper. Research concepts developed this paper are mainly from the technical report "Numerical LTL synthesis for cyber-physical systems", coauthored by Chih-Hong Cheng (ABB Research) and Edward A. Lee (UC Berkeley)

Certification for mu-calculus with winning strategies

Authors: Martin Hofmann, Harald Ruess

Abstract: We define memory-efficient certificates for $μ$-calculus model checking problems based on the well-known correspondence of the $μ$-calculus model checking with winning certain parity games. Winning strategies can independently checked, in low polynomial time, by observing that there is no reachable strongly connected component in the graph of the parity game whose largest priority is odd. Winning… ▽ More We define memory-efficient certificates for $μ$-calculus model checking problems based on the well-known correspondence of the $μ$-calculus model checking with winning certain parity games. Winning strategies can independently checked, in low polynomial time, by observing that there is no reachable strongly connected component in the graph of the parity game whose largest priority is odd. Winning strategies are computed by fixpoint iteration following the naive semantics of $μ$-calculus. We instrument the usual fixpoint iteration of $μ$-calculus model checking so that it produces evidence in the form of a winning strategy; these winning strategies can be computed in polynomial time in $|S|$ and in space $O(|S|^2 |φ|^2)$, where $|S|$ is the size of the state space and $|φ|$ the length of the formula $φ$\@. The main technical contribution here is the notion and algebra of partial winning strategies. On the technical level our work can be seen as a new, simpler, and immediate constructive proof of the correspondence between $μ$-calculus and parity games. △ Less

Submitted 8 January, 2014; originally announced January 2014.

Comments: Presented at the VeriSure workshop associated with CAV'13 in St. Petersburg in July 2013

Security policies for distributed systems

Authors: Jean Quilbeuf, Georgeta Igna, Denis Bytschkow, Harald Ruess

Abstract: A security policy specifies a security property as the maximal information flow. A distributed system composed of interacting processes implicitly defines an intransitive security policy by repudiating direct information flow between processes that do not exchange messages directly. We show that implicitly defined security policies in distributed systems are enforced, provided that processes run i… ▽ More A security policy specifies a security property as the maximal information flow. A distributed system composed of interacting processes implicitly defines an intransitive security policy by repudiating direct information flow between processes that do not exchange messages directly. We show that implicitly defined security policies in distributed systems are enforced, provided that processes run in separation, and possible process communication on a technical platform is restricted to specified message paths of the system. Furthermore, we propose to further restrict the allowable information flow by adding filter functions for controlling which messages may be transmitted between processes, and we prove that locally checking filter functions is sufficient for ensuring global security policies. Altogether, global intransitive security policies are established by means of local verification conditions for the (trusted) processes of the distributed system. Moreover, security policies may be implemented securely on distributed integration platforms which ensure partitioning. We illustrate our results with a smart grid case study, where we use CTL model checking for discharging local verification conditions for each process under consideration. △ Less

Submitted 14 October, 2013; originally announced October 2013.

Comments: Submitted to POST14

On Behavioral Types for OSGi: From Theory to Implementation

Authors: Jan Olaf Blech, Harald Rueß, Bernhard Schätz

Abstract: This report presents our work on behavioral types for OSGi component systems. It extends previously published work and presents features and details that have not yet been published. In particular, we cover a discussion on behavioral types in general, and Eclipse based implementation work on behavioral types . The implementation work covers: editors, means for comparing types at development and ru… ▽ More This report presents our work on behavioral types for OSGi component systems. It extends previously published work and presents features and details that have not yet been published. In particular, we cover a discussion on behavioral types in general, and Eclipse based implementation work on behavioral types . The implementation work covers: editors, means for comparing types at development and runtime, a tool connection to resolve incompatibilities, and an AspectJ based infrastructure to ensure behavioral type correctness at runtime of a system. Furthermore, the implementation comprises various auxiliary operations. We present some evaluation work based on examples. △ Less

Submitted 25 June, 2013; originally announced June 2013.

Comments: arXiv admin note: text overlap with arXiv:1302.5175

EFSMT: A Logical Framework for Cyber-Physical Systems

Authors: Chih-Hong Cheng, Natarajan Shankar, Harald Ruess, Saddek Bensalem

Abstract: The design of cyber-physical systems is challenging in that it includes the analysis and synthesis of distributed and embedded real-time systems for controlling, often in a nonlinear way, the environment. We address this challenge with EFSMT, the exists-forall quantified first-order fragment of propositional combinations over constraints (including nonlinear arithmetic), as the logical framework a… ▽ More The design of cyber-physical systems is challenging in that it includes the analysis and synthesis of distributed and embedded real-time systems for controlling, often in a nonlinear way, the environment. We address this challenge with EFSMT, the exists-forall quantified first-order fragment of propositional combinations over constraints (including nonlinear arithmetic), as the logical framework and foundation for analyzing and synthesizing cyber-physical systems. We demonstrate the expressiveness of EFSMT by reducing a number of pivotal verification and synthesis problems to EFSMT. Exemplary problems in this paper include synthesis for robust control via BIBO stability, Lyapunov coefficient finding for nonlinear control systems, distributed priority synthesis for orchestrating system components, and synthesis for hybrid control systems. We are also proposing an algorithm for solving EFSMT problems based on the interplay between two SMT solvers for respectively solving universally and existentially quantified problems. This algorithms builds on commonly used techniques in modern SMT solvers, and generalizes them to quantifier reasoning by counterexample-guided constraint strengthening. The EFSMT solver uses Bernstein polynomials for solving nonlinear arithmetic constraints. △ Less

Submitted 14 June, 2013; originally announced June 2013.

Distributed Priority Synthesis

Authors: Chih-Hong Cheng, Rongjie Yan, Saddek Bensalem, Harald Ruess

Abstract: Given a set of interacting components with non-deterministic variable update and given safety requirements, the goal of priority synthesis is to restrict, by means of priorities, the set of possible interactions in such a way as to guarantee the given safety conditions for all possible runs. In distributed priority synthesis we are interested in obtaining local sets of priorities, which are de… ▽ More Given a set of interacting components with non-deterministic variable update and given safety requirements, the goal of priority synthesis is to restrict, by means of priorities, the set of possible interactions in such a way as to guarantee the given safety conditions for all possible runs. In distributed priority synthesis we are interested in obtaining local sets of priorities, which are deployed in terms of local component controllers sharing intended next moves between components in local neighborhoods only. These possible communication paths between local controllers are specified by means of a communication architecture. We formally define the problem of distributed priority synthesis in terms of a multi-player safety game between players for (angelically) selecting the next transition of the components and an environment for (demonically) updating uncontrollable variables. We analyze the complexity of the problem, and propose several optimizations including a solution-space exploration based on a diagnosis method using a nested extension of the usual attractor computation in games together with a reduction to corresponding SAT problems. When diagnosis fails, the method proposes potential candidates to guide the exploration. These optimized algorithms for solving distributed priority synthesis problems have been integrated into the VissBIP framework. An experimental validation of this implementation is performed using a range of case studies including scheduling in multicore processors and modular robotics. △ Less

Submitted 26 November, 2012; originally announced November 2012.

Comments: In Proceedings SSV 2012, arXiv:1211.5873

Journal ref: EPTCS 102, 2012, pp. 57-72

Distributed Priority Synthesis and its Applications

Authors: Chih-Hong Cheng, Saddek Bensalem, Rongjie Yan, Harald Ruess, Christian Buckl, Alois Knoll

Abstract: Given a set of interacting components with non-deterministic variable update and given safety requirements, the goal of priority synthesis is to restrict, by means of priorities, the set of possible interactions in such a way as to guarantee the given safety conditions for all possible runs. In distributed priority synthesis we are interested in obtaining local sets of priorities, which are deploy… ▽ More Given a set of interacting components with non-deterministic variable update and given safety requirements, the goal of priority synthesis is to restrict, by means of priorities, the set of possible interactions in such a way as to guarantee the given safety conditions for all possible runs. In distributed priority synthesis we are interested in obtaining local sets of priorities, which are deployed in terms of local component controllers sharing intended next moves between components in local neighborhoods only. These possible communication paths between local controllers are specified by means of a communication architecture. We formally define the problem of distributed priority synthesis in terms of a multi-player safety game between players for (angelically) selecting the next transition of the components and an environment for (demonically) updating uncontrollable variables; this problem is NP-complete. We propose several optimizations including a solution-space exploration based on a diagnosis method using a nested extension of the usual attractor computation in games together with a reduction to corresponding SAT problems. When diagnosis fails, the method proposes potential candidates to guide the exploration. These optimized algorithms for solving distributed priority synthesis problems have been integrated into our VissBIP framework. An experimental validation of this implementation is performed using a range of case studies including scheduling in multicore processors and modular robotics. △ Less

Submitted 27 January, 2012; v1 submitted 8 December, 2011; originally announced December 2011.

Comments: 1. Timestamp the joint work "Distributed Priority Synthesis" from four institutes (Verimag, TUM, ISCAS, fortiss). 2. This version (v.2) updates related work in distributed synthesis

Algorithms for Synthesizing Priorities in Component-based Systems

Authors: Chih-Hong Cheng, Saddek Bensalem, Yu-Fang Chen, Rongjie Yan, Barbara Jobstmann, Harald Ruess, Christian Buckl, Alois Knoll

Abstract: We present algorithms to synthesize component-based systems that are safe and deadlock-free using priorities, which define stateless-precedence between enabled actions. Our core method combines the concept of fault-localization (using safety-game) and fault-repair (using SAT for conflict resolution). For complex systems, we propose three complementary methods as preprocessing steps for priority sy… ▽ More We present algorithms to synthesize component-based systems that are safe and deadlock-free using priorities, which define stateless-precedence between enabled actions. Our core method combines the concept of fault-localization (using safety-game) and fault-repair (using SAT for conflict resolution). For complex systems, we propose three complementary methods as preprocessing steps for priority synthesis, namely (a) data abstraction to reduce component complexities, (b) alphabet abstraction and #-deadlock to ignore components, and (c) automated assumption learning for compositional priority synthesis. △ Less

Submitted 7 October, 2011; v1 submitted 6 July, 2011; originally announced July 2011.

Comments: Full version of the ATVA'11 paper (compared to the 1st arXiv version, we add one additional sentence to avoid confusion)

A Game-theoretic Approach for Synthesizing Fault-Tolerant Embedded Systems

Authors: Chih-Hong Cheng, Harald Ruess, Alois Knoll, Christian Buckl

Abstract: In this paper, we present an approach for fault-tolerant synthesis by combining predefined patterns for fault-tolerance with algorithmic game solving. A non-fault-tolerant system, together with the relevant fault hypothesis and fault-tolerant mechanism templates in a pool are translated into a distributed game, and we perform an incomplete search of strategies to cope with undecidability. The resu… ▽ More In this paper, we present an approach for fault-tolerant synthesis by combining predefined patterns for fault-tolerance with algorithmic game solving. A non-fault-tolerant system, together with the relevant fault hypothesis and fault-tolerant mechanism templates in a pool are translated into a distributed game, and we perform an incomplete search of strategies to cope with undecidability. The result of the game is translated back to executable code concretizing fault-tolerant mechanisms using constraint solving. The overall approach is implemented to a prototype tool chain and is illustrated using examples. △ Less

Submitted 1 November, 2010; originally announced November 2010.

Comments: The extended version of the paper "Synthesis of Fault-Tolerant Embedded Systems using Games: from Theory to Practice" in VMCAI'11

Age of the Universe: Influence of the Inhomogeneities on the global Expansion-Factor

Authors: H. Russ, M. H. Soffel, M. Kasai, G. Börner

Abstract: For the first time we calculate quantitatively the influence of inhomogeneities on the global expansion factor by averaging the Friedmann equation. In the framework of the relativistic second-order Zel'dovich-approximation scheme for irrotational dust we use observational results in form of the normalisation constant fixed by the COBE results and we check different power spectra, namely for adia… ▽ More For the first time we calculate quantitatively the influence of inhomogeneities on the global expansion factor by averaging the Friedmann equation. In the framework of the relativistic second-order Zel'dovich-approximation scheme for irrotational dust we use observational results in form of the normalisation constant fixed by the COBE results and we check different power spectra, namely for adiabatic CDM, isocurvature CDM, HDM, WDM, Strings and Textures. We find that the influence of the inhomogeneities on the global expansion factor is very small. So the error in determining the age of the universe using the Hubble constant in the usual way is negligible. This does not imply that the effect is negligible for local astronomical measurements of the Hubble constant. Locally the determination of the redshift-distance relation can be strongly influenced by the peculiar velocity fields due to inhomogeneities. Our calculation does not consider such effects, but is contrained to comparing globally homogeneous and averaged inhomogeneous matter distributions. In addition we relate our work to previous treatments. △ Less

Submitted 27 May, 1997; v1 submitted 23 December, 1996; originally announced December 1996.

Comments: 10 pages, version accepted by Phys. Rev. D

Journal ref: Phys.Rev. D56 (1997) 2044-2050

The Zel'dovich-type approximation for an inhomogeneous universe in general relativity: second-order solutions

Authors: H. Russ, M. Morita, M. Kasai, G. Boerner

Abstract: The gravitational instability of inhomogeneities in the expanding universe is studied by the relativistic second-order approximation. Using the tetrad formalism we consider irrotational dust universes and get equations very similar to those given in the Lagrangian perturbation theory in Newtonian cosmology. Neglecting the cosmological constant and assuming a flat background model we give the sol… ▽ More The gravitational instability of inhomogeneities in the expanding universe is studied by the relativistic second-order approximation. Using the tetrad formalism we consider irrotational dust universes and get equations very similar to those given in the Lagrangian perturbation theory in Newtonian cosmology. Neglecting the cosmological constant and assuming a flat background model we give the solutions of the nonlinear dynamics of cosmological perturbations. We present the complete second-order solutions, which extend and improve earlier works. △ Less

Submitted 12 December, 1995; originally announced December 1995.

Comments: 20 pages, LaTeX, no figures

Report number: DM5647

Journal ref: Phys.Rev. D53 (1996) 6881-6888