scholarly journals ARCH-COMP18 Category Report: Hybrid Systems Theorem Proving

10.29007/vjh3 ◽  
2018 ◽  
Author(s):  
Stefan Mitsch ◽  
Andrew Sogokon ◽  
Yong Kiam Tan ◽  
André Platzer ◽  
Hengjun Zhao ◽  
...  
Keyword(s):  
Programming Languages ◽  
Hybrid Systems ◽  
Hybrid System ◽  
Theorem Proving ◽  
Proof Checking ◽  
Specific Advice ◽  
Additional Input ◽  
Safety Specification ◽  
Experimental Findings ◽  
Friendly Competition

This paper reports on establishing Hybrid Systems Theorem Proving (HSTP) as a new category in the ARCH-COMP Friendly Competition 2018. The most important char- acteristic features of the HSTP category are: i) The flexibility of programming languages as structuring principles for hybrid systems, ii) The unambiguity and precision of program semantics, and iii) The mathematical rigor of logical reasoning principles. The HSTP category especially features many nonlinear and parametric continuous and hybrid sys- tems. Owing to the nature of theorem proving, HSTP is able to accomodate three modes: A) Automatic in which the entire verification is performed fully automatically without any additional input beyond the original hybrid system and its safety specification. H) Hints in which select proof hints are provided as part of the input problem specification, allowing users to communicate specific advice about the system such as loop invariants. S) Scripted in which a significant part of the verification is done with dedicated proof scripts or problem-specific proof tactics. This threefold split makes it possible to better identify the sources of scalability and efficiency bottlenecks in hybrid systems theorem proving. The existence of all three categories also makes it easier for new tools with a different focus to participate in the competition, wherever they focus on in the spectrum from fast proof checking all the way to full automation. The types of benchmarks considered and experimental findings are described in this paper as well.

scholarly journals ARCH-COMP19 Category Report: Hybrid Systems Theorem Proving

10.29007/nrv8 ◽  
2019 ◽  
Author(s):  
Stefan Mitsch ◽  
Andrew Sogokon ◽  
Yong Kiam Tan ◽  
Xiangyu Jin ◽  
Bohua Zhan ◽  
...  
Keyword(s):  
Programming Languages ◽  
Hybrid Systems ◽  
Theorem Proving ◽  
Proof Checking ◽  
Specific Advice ◽  
Previous Edition ◽  
Additional Input ◽  
Safety Specification ◽  
Characteristic Features ◽  
Experimental Findings

This paper reports on the Hybrid Systems Theorem Proving (HSTP) category in the ARCH-COMP Friendly Competition 2019. The most important characteristic features of the HSTP category remain as in the previous edition [MST+18]: i) The flexibility of programming languages as structuring principles for hybrid systems, ii) The unambiguity and precision of program semantics, and iii) The mathematical rigor of logical reason- ing principles. The HSTP category especially features many nonlinear and parametric continuous and hybrid systems. Owing to the nature of theorem proving, HSTP again accommodates three modes: A) Automatic in which the entire verification is performed fully automatically without any additional input beyond the original hybrid system and its safety specification. H) Hints in which select proof hints are provided as part of the input problem specification, allowing users to communicate specific advice about the system such as loop invariants. S) Scripted in which a significant part of the verification is done with dedicated proof scripts or problem-specific proof tactics. This threefold split makes it possible to better identify the sources of scalability and efficiency bottlenecks in hybrid systems theorem proving. The existence of all three categories also makes it easier for new tools with a different focus to participate in the competition, wherever they focus on in the spectrum from fast proof checking all the way to full automation. The types of benchmarks considered and experimental findings are described in this paper as well.

scholarly journals ARCH-COMP20 Category Report:Hybrid Systems Theorem Proving

10.29007/bdq9 ◽  
2020 ◽  
Author(s):  
Stefan Mitsch ◽  
Jonathan Julián Huerta Y Munive ◽  
Xiangyu Jin ◽  
Bohua Zhan ◽  
Shuling Wang ◽  
...  
Keyword(s):  
Hybrid Systems ◽  
Theorem Proving ◽  
Proof Checking ◽  
Specific Advice ◽  
Additional Input ◽  
Logical Reason ◽  
Safety Specification ◽  
Characteristic Features ◽  
Experimental Findings ◽  
Friendly Competition

This paper reports on the Hybrid Systems Theorem Proving (HSTP) category in the ARCH-COMP Friendly Competition 2020. The characteristic features of the HSTP category remain as in the previous editions [MST+18, MST+19]: i) The flexibility of pro- gramming languages as structuring principles for hybrid systems, ii) The unambiguity and precision of program semantics, and iii) The mathematical rigor of logical reason- ing principles. The HSTP category especially features many nonlinear and parametric continuous and hybrid systems. Owing to the nature of theorem proving, HSTP again accommodates three modes: A) Automatic in which the entire verification is performed fully automatically without any additional input beyond the original hybrid system and its safety specification. H) Hints in which select proof hints are provided as part of the input problem specification, allowing users to communicate specific advice about the sys- tem such as loop invariants. S) Scripted in which a significant part of the verification is done with dedicated proof scripts or problem-specific proof tactics. This threefold split makes it possible to better identify the sources of scalability and efficiency bottlenecks in hybrid systems theorem proving. The existence of all three categories also makes it easier for new tools with a different focus to participate in the competition, wherever they focus on in the spectrum from fast proof checking all the way to full automation. The types of benchmarks considered and experimental findings with the participating theorem provers KeYmaera, KeYmaera X 4.6.3, KeYmaera X 4.8.0, Isabelle/HOL/Hybrid-Systems-VCs, and HHL Prover are described in this paper as well.

Autonomy and Responsibility in Hybrid Systems

2017 ◽  
Author(s):  
Wulf Loh ◽  
Janina Loh
Keyword(s):  
Hybrid Systems ◽  
Hybrid System ◽  
Moral Dilemma ◽  
Autonomous Driving ◽  
Shared Responsibility ◽  
Driving System ◽  
Autonomous Cars ◽  
Self Driving Cars ◽  
Trolley Cases ◽  
Autonomous Driving System

In this chapter, we give a brief overview of the traditional notion of responsibility and introduce a concept of distributed responsibility within a responsibility network of engineers, driver, and autonomous driving system. In order to evaluate this concept, we explore the notion of man–machine hybrid systems with regard to self-driving cars and conclude that the unit comprising the car and the operator/driver consists of such a hybrid system that can assume a shared responsibility different from the responsibility of other actors in the responsibility network. Discussing certain moral dilemma situations that are structured much like trolley cases, we deduce that as long as there is something like a driver in autonomous cars as part of the hybrid system, she will have to bear the responsibility for making the morally relevant decisions that are not covered by traffic rules.

Bayesian hybrid automata: Reconciling formal methods with metrology

2021 ◽  
Vol 0 (0) ◽  
Author(s):  
Paul Kröger ◽  
Martin Fränzle
Keyword(s):  
System Dynamics ◽  
Hybrid Systems ◽  
Hybrid System ◽  
Formal Model ◽  
Continuous Control ◽  
Hybrid Automata ◽  
Physical Processes ◽  
Natural Domain ◽  
State Tracking ◽  
Smart Technologies

Abstract Hybrid system dynamics arises when discrete actions meet continuous behaviour due to physical processes and continuous control. A natural domain of such systems are emerging smart technologies which add elements of intelligence, co-operation, and adaptivity to physical entities. Various flavours of hybrid automata have been suggested as a means to formally analyse dynamics of such systems. In this article, we present our current work on a revised formal model that is able to represent state tracking and estimation in hybrid systems and thereby enhancing precision of verification verdicts.

Fuel-Cell Hybrid Systems to Generate Shipboard Electrical Power

2009 ◽  
Author(s):  
W. J. Sembler ◽  
S. Kumar
Keyword(s):  
Fuel Cells ◽  
Fuel Cell ◽  
Air Quality ◽  
Hybrid Systems ◽  
Hybrid System ◽  
Cell Hybrid ◽  
Electrical Power ◽  
History Of ◽  
Marine Applications ◽  
Fuel Cell Hybrid

The reduction of shipboard airborne emissions has been receiving increased attention due to the desire to improve air quality and reduce the generation of greenhouse gases. The use of a fuel cell could represent an environmentally friendly way for a ship to generate in-port electrical power that would eliminate the need to operate diesel-driven generators or use shore power. This paper includes a brief description of the various types of fuel cells in use today, together with a review of the history of fuel cells in marine applications. In addition, the results of a feasibility study conducted to evaluate the use of a fuel-cell hybrid system to produce shipboard electrical power are presented.

scholarly journals Optimal Sizing of a Pv-Wind Hybrid System Using Measured and Generated Database

2021 ◽  
Vol 03 (01) ◽  
pp. 34-44
Author(s):  
Abdellah Benallal ◽  
◽  
Nawel Cheggaga ◽  
Keyword(s):  
Renewable Energy ◽  
Wind Speed ◽  
Wind Turbine ◽  
Hybrid Systems ◽  
Hybrid System ◽  
Measured Data ◽  
Electrical Load ◽  
Wind Potential ◽  
Simulation Results ◽  
The Cost

Renewable energy hybrid systems give a good solution in isolated sites, in the Algerian desert; wind and solar potentials are considerably perfect for a combination in a renewable energy hybrid system to satisfy local village electrical load and minimize the storage requirements, which leads to reduce the cost of the installation. For a good sizing, it is essential to know accurately the solar potential of the installation area also wind potential at the same height where wind electric generators will be placed. In this work, we optimize a completely autonomous PV-wind hybrid system and show the techno-economical effects of the height of the wind turbine on the sizing of the hybrid system. We also compare the simulation results obtained from using wind speed measured data at 10 meters and 40 meters of height with the ones obtained from using wind speed extrapolation on HOMER software.

scholarly journals ARCH-COMP17 Repeatability Evaluation Report

10.29007/7hvk ◽  
2018 ◽  
Author(s):  
Taylor T. Johnson
Keyword(s):  
Formal Verification ◽  
Hybrid Systems ◽  
Benchmark Problems ◽  
Safety Verification ◽  
Evaluation Report ◽  
Standard Practice ◽  
Friendly Competition

This report presents the results of the repeatability evaluation for a friendly competition for formal verification of continuous and hybrid systems. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2017. In its first edition, thirteen tools have been applied to solve benchmark problems for the six competition categories, of which, ten tools were evaluated and passed the repeatability evaluation. The repeatability results represent a snapshot of the current landscape of tools and the types of benchmarks for which they are particularly suited and for which others may repeat their analyses. Due to the diversity of problems in verification of continuous and hybrid systems, as well as basing on standard practice in repeatability evaluations, we evaluate the tools with pass and/or failing being repeatable. These re- sults probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems up to this date.

scholarly journals Subtree matching by pushdown automata

2010 ◽  
Vol 7 (2) ◽  
pp. 331-357 ◽  
Author(s):  
Tomás Flouri ◽  
Jan Janousek ◽  
Bořivoj Melichar
Keyword(s):  
Programming Languages ◽  
Theorem Proving ◽  
Systematic Approach ◽  
Finite Automata ◽  
Term Rewriting ◽  
Mechanical Theorem Proving ◽  
Pushdown Automaton ◽  
String Pattern ◽  
Pushdown Automata ◽  
Mechanical Theorem

Subtree matching is an important problem in Computer Science on which a number of tasks, such as mechanical theorem proving, term-rewriting, symbolic computation and nonprocedural programming languages are based on. A systematic approach to the construction of subtree pattern matchers by deterministic pushdown automata, which read subject trees in prefix and postfix notation, is presented. The method is analogous to the construction of string pattern matchers: for a given pattern, a nondeterministic pushdown automaton is created and is then determinised. In addition, it is shown that the size of the resulting deterministic pushdown automata directly corresponds to the size of the existing string pattern matchers based on finite automata.

Condition-based opportunistic maintenance policy for a series–parallel hybrid system with economic dependence

2021 ◽  
Vol ahead-of-print (ahead-of-print) ◽  
Author(s):  
Aiping Jiang ◽  
Zhenni Huang ◽  
Jiahui Xu ◽  
Xuemin Xu
Keyword(s):  
Hybrid Systems ◽  
Hybrid System ◽  
Maintenance Policy ◽  
Economic Dependence ◽  
Opportunistic Maintenance ◽  
Content Type ◽  
Cost Rate ◽  
Parallel Hybrid ◽  
In Series ◽  
Redundant Structure

PurposeThe purpose of this paper is to propose a condition-based opportunistic maintenance policy considering economic dependence for a series–parallel hybrid system with a K-out-of-N redundant structure, where a single component in series is denoted as subsystem1, and K-out-of-N redundant structure is denoted as subsystem2.Design/methodology/approachBased on the theory of Residual Useful Life (RUL), inspection points are determined, and then different maintenance actions are adopted in the purpose of minimizing the cost rate. Both perfect and imperfect maintenance actions are carried out for subsystem1. More significantly, regarding economic dependence, condition-based opportunistic maintenance is designed for the series–parallel hybrid system: preemptive maintenance for subsystem1, and both preemptive and postponed maintenance for subsystem2.FindingsThe sensitivity analysis indicates that the proposed policy outperforms two classical maintenance policies, incurring the lowest total cost rate under the context of both heterogeneous and quasi-homogeneous K-out-of-N subsystems.Practical implicationsThis model can be applied in series–parallel systems with redundant structures that are widely used in power transmission systems in electric power plants, manufacturing systems in textile factories and sewerage systems. Considering inconvenience and high cost incurred in the inspection of hybrid systems, this model helps production managers better maintain these systems.Originality/valueIn maintenance literature, much attention has been received in repairing strategies on hybrid systems with economic dependence considering preemptive maintenance. Limited work has considered postponed maintenance. However, this paper uses both condition-based preemptive and postponed maintenance on the issue of economic dependence bringing opportunities for grouping maintenance activities for a series–parallel hybrid system.

Sign in / Sign up

Export Citation Format

Share Document