Searcharxiv⌕ Search

arXiv subjects

Zhiming Liu

Publications and source records attributed to Zhiming Liu.

48 records · Page 3Linked to original sources

Learning Safe Neural Network Controllers with Barrier Certificates

We provide a novel approach to synthesize controllers for nonlinear continuous dynamical systems with control against safety properties. The controllers are based on neural networks (NNs). To certify the safety property we utilize barrier functions, which are represented by NNs as well. We train the controller-NN and barrier-NN simultaneously, achieving a verification-in-the-loop synthesis. We provide a prototype tool nncontroller with a number of case studies. The experiment results confirm the feasibility and efficacy of our approach.

eess.SY↗

Solving Splitted Multi-Commodity Flow Problem by Efficient Linear Programming Algorithm

Column generation is often used to solve multi-commodity flow problems. A program for column generation always includes a module that solves a linear equation. In this paper, we address three major issues in solving linear problem during column generation procedure which are (1) how to employ the sparse property of the coefficient matrix; (2) how to reduce the size of the coefficient matrix; and (3) how to reuse the solution to a similar equation. To this end, we first analyze the sparse property of coefficient matrix of linear equations and find that the matrices occurring in iteration are very sparse. Then, we present an algorithm locSolver (for localized system solver) for linear equations with sparse coefficient matrices and right-hand-sides. This algorithm can reduce the number of variables. After that, we present the algorithm incSolver (for incremental system solver) which utilizes similarity in the iterations of the program for a linear equation system. All three techniques can be used in column generation of multi-commodity problems. Preliminary numerical experiments show that the incSolver is significantly faster than the existing algorithms. For example, random test cases show that incSolver is at least 37 times and up to 341 times faster than popular solver LAPACK.

math.OC↗

Parameter Synthesis Problems for Parametric Timed Automata

We consider the parameter synthesis problem of parametric timed automata (PTAs). The problem is, given a PTA and a property, to compute the set of valuations of the parameters under which the resulting timed automaton satisfies the property. Such a set of parameter valuations is called a feasible region for the PTA and the property. The problem is known undecidable in general. This paper, however, presents our study on some decidable sub-classes of PTAs and proposes efficient parameter synthesis algorithms for them.

eess.SY↗

Deep Learning with Long Short-Term Memory for Time Series Prediction

Time series prediction can be generalized as a process that extracts useful information from historical records and then determines future values. Learning long-range dependencies that are embedded in time series is often an obstacle for most algorithms, whereas Long Short-Term Memory (LSTM) solutions, as a specific kind of scheme in deep learning, promise to effectively overcome the problem. In this article, we first give a brief introduction to the structure and forward propagation mechanism of the LSTM model. Then, aiming at reducing the considerable computing cost of LSTM, we put forward the Random Connectivity LSTM (RCLSTM) model and test it by predicting traffic and user mobility in telecommunication networks. Compared to LSTM, RCLSTM is formed via stochastic connectivity between neurons, which achieves a significant breakthrough in the architecture formation of neural networks. In this way, the RCLSTM model exhibits a certain level of sparsity, which leads to an appealing decrease in the computational complexity and makes the RCLSTM model become more applicable in latency-stringent application scenarios. In the field of telecommunication networks, the prediction of traffic series and mobility traces could directly benefit from this improvement as we further demonstrate that the prediction accuracy of RCLSTM is comparable to that of the conventional LSTM no matter how we change the number of training samples or the length of input sequences.

cs.NE↗

Parameter Synthesis Problems for one parametric clock Timed Automata

In this paper, we study the parameter synthesis problem for a class of parametric timed automata. The problem asks to construct the set of valuations of the parameters in the parametric timed automa- ton, referred to as the feasible region, under which the resulting timed automaton satisfies certain properties. We show that the parameter syn- thesis problem of parametric timed automata with only one parametric clock (unlimited concretely constrained clock) and arbitrarily many pa- rameters is solvable when all the expressions are linear expressions. And it is moreover the synthesis problem is solvable when the form of con- straints are parameter polynomial inequality not just simple constraint and parameter domain is nonnegative real number.

cs.FL↗

Automated Prototype Generation from Formal Requirements Model

Prototyping is an effective and efficient way of requirement validation to avoid introducing errors in the early stage of software development. However, manually developing a prototype of a software system requires additional efforts, which would increase the overall cost of software development. In this paper, we present an approach with a developed tool to automatic generation of prototypes from formal requirements models. A requirements model consists of a use case diagram, a conceptual class diagram, use case definitions specified by system sequence diagrams and the contracts of their system operations. We propose a method to decompose a contract into executable parts and non-executable parts. A set of transformation rules is given to decompose the executable part into pre-implemented primitive operations. A non-executable part is usually realized by significant algorithms such as sorting a list, finding the shortest path or domain-specific computation. It can be implemented manually or by using existing code. A CASE tool is developed that provides an interface for developers to develop a program for each non-executable part of a contract, and automatically transforms the executables into sequences of pre-implemented primitive operations. We have conducted four cases studies with over 50 use cases. The experimental result shows that the 93.65% of requirement specifications are executable, and only 6.35% are non-executable such as sorting and event-call, which can be implemented by developers manually or invoking the APIs of advanced algorithms in Java library. The one second generated the prototype of a case study requires approximate nine hours manual implementation by a skilled programmer. Overall, the result is satisfiable, and the proposed approach with the developed CASE tool can be applied to the software industry for requirements engineering.

cs.SE↗

Traffic Prediction Based on Random Connectivity in Deep Learning with Long Short-Term Memory

Traffic prediction plays an important role in evaluating the performance of telecommunication networks and attracts intense research interests. A significant number of algorithms and models have been put forward to analyse traffic data and make prediction. In the recent big data era, deep learning has been exploited to mine the profound information hidden in the data. In particular, Long Short-Term Memory (LSTM), one kind of Recurrent Neural Network (RNN) schemes, has attracted a lot of attentions due to its capability of processing the long-range dependency embedded in the sequential traffic data. However, LSTM has considerable computational cost, which can not be tolerated in tasks with stringent latency requirement. In this paper, we propose a deep learning model based on LSTM, called Random Connectivity LSTM (RCLSTM). Compared to the conventional LSTM, RCLSTM makes a notable breakthrough in the formation of neural network, which is that the neurons are connected in a stochastic manner rather than full connected. So, the RCLSTM, with certain intrinsic sparsity, have many neural connections absent (distinguished from the full connectivity) and which leads to the reduction of the parameters to be trained and the computational cost. We apply the RCLSTM to predict traffic and validate that the RCLSTM with even 35% neural connectivity still shows a satisfactory performance. When we gradually add training samples, the performance of RCLSTM becomes increasingly closer to the baseline LSTM. Moreover, for the input traffic sequences of enough length, the RCLSTM exhibits even superior prediction accuracy than the baseline LSTM.

cs.NI↗

MedShare: Medical Resource Sharing among Autonomous Healthcare Providers

Legacy Electronic Health Records (EHRs) systems were not developed with the level of connectivity expected from them nowadays. Therefore, interoperability weakness inherent in the legacy systems can result in poor patient care and waste of financial resources. Large hospitals are less likely to share their data with external hospitals due to economic and political reasons. Motivated by these facts, we aim to provide a set of software implementation guidelines, i.e., MedShare to deal with interoperability issues among disconnected healthcare systems. The proposed integrated architecture includes: 1) a data extractor to fetch legacy medical data from a hemodialysis center, 2) converting it to a common data model, 3) indexing patient information using the HashMap technique, and 4) a set of services and tools that can be installed as a coherent environment on top of stand-alone EHRs systems. Our work enabled three cooperating but autonomous hospitals to mutually exchange medical data and helped them develop a common reference architecture. It lets stakeholders retain control over their patient data, winning the trust and confidence much needed towards a successful deployment of MedShare. Security concerns were effectively addressed that also included patient consent in the data exchange process. Thereby, the implemented toolset offered a collaborative environment to share EHRs by the healthcare providers.

cs.SE↗

Anonymously Analyzing Clinical Datasets

This paper takes on the problem of automatically identifying clinically-relevant patterns in medical datasets without compromising patient privacy. To achieve this goal, we treat datasets as a black box for both internal and external users of data that lets us handle clinical data queries directly and far more efficiently. The novelty of the approach lies in avoiding the data de-identification process often used as a means of preserving patient privacy. The implemented toolkit combines software engineering technologies such as Java EE and RESTful web services, to allow exchanging medical data in an unidentifiable XML format as well as restricting users to the need-to-know principle. Our technique also inhibits retrospective processing of data, such as attacks by an adversary on a medical dataset using advanced computational methods to reveal Protected Health Information (PHI). The approach is validated on an endoscopic reporting application based on openEHR and MST standards. From the usability perspective, the approach can be used to query datasets by clinical researchers, governmental or non-governmental organizations in monitoring health care services to improve quality of care.

cs.SE↗

A Framework for Automated and Certified Refinement Steps

The refinement calculus provides a methodology for transforming an abstract specification into a concrete implementation, by following a succession of refinement rules. These rules have been mechanized in theorem-provers, thus providing a formal and rigorous way to prove that a given program refines another one. In a previous work, we have extended this mechanization for object-oriented programs, where the memory is represented as a graph, and we have integrated our approach within the rCOS tool, a model-driven software development tool providing a refinement language. Hence, for any refinement step, the tool automatically generates the corresponding proof obligations and the user can manually discharge them, using a provided library of refinement lemmas. In this work, we propose an approach to automate the search of possible refinement rules from a program to another, using the rewriting tool Maude. Each refinement rule in Maude is associated with the corresponding lemma in Isabelle, thus allowing the tool to automatically generate the Isabelle proof when a refinement rule can be automatically found. The user can add a new refinement rule by providing the corresponding Maude rule and Isabelle lemma.

cs.SE↗

Ab initio investigation of optical properties of high-pressure phases of ice

We report a detailed ab initio investigation on the optical properties of ice under a wide high pressure range. The ice X phase (up to 380GPa), the theoretical proposed higher pressure phase ice XV (300GPa), as well as the ambient pressure low-temperature phase ice XI are involved. Our results show that the dispersion relations of optical properties of ice under high pressure are quite different from those under ambient pressure. Under higher pressure, there is whole tendency of blue shift in all optical properties of ice, and the energy region for optical response become broader, such as the absorption band and reflection band. In addition to the augmented absorption edge, all absorption peaks are found to be rising, and the reflection peaks are also enhanced a bit; hence the transmissivity of ice is inferred to be dropping. The photoconductivity is enhanced, and we explain this behavior from the increase of earner density. The static optical properties are found to be pressure independent, and principally due to the network topology of hydrogen bonding.

cond-mat.mtrl-sci↗

Ab initio investigation of hydrogen bonding and electronic structure of high-pressure phases of ice

We report a detailed ab initio investigation on hydrogen bonding, geometry, electronic structure, and lattice dynamics of ice under a large high pressure range, including the ice X phase (55-380GPa), the previous theoretically proposed higher-pressure phase ice XIIIM (Refs. 1-2) (380GPa), ice XV (a new structure we derived from ice XIIIM) (300-380GPa), as well as the ambient pressure low-temperature phase ice XI. Different from many other materials, the band gap of ice X is found to be increasing linearly with pressure from 55GPa up to 290GPa, the electronic density of states (DOS) shows that the valence bands have a tendency of red shift (move to lower energies) referring to the Fermi energy while the conduction bands have a blue shift (move to higher energies). This behavior is interpreted as the high pressure induced change of s-p charge transfers between hydrogen and oxygen. It is found that ice X exists in the pressure range from 75GPa to about 290GPa. Beyond 300GPa, a new hydrogen-bonding structure with 50% hydrogen atoms in symmetric positions in O-H-O bonds and the other half being asymmetric, ice XV, is identified. The physical mechanism for this broken symmetry in hydrogen bonding is revealed.

cond-mat.mtrl-sci↗