People-counting data can be used in building-control systems to improve comfort and in space management applications to optimize building space. In this work, we consider a combi-sensor with a single-pixel thermopile and passive infrared sensor for people counting. We first develop a thermopile signal model for object temperature measurements under multiple people occupancy. We then propose a people counting method based on: cumulative sum (CUSUM) change detection in the object temperature signal, forming a people count estimate using likelihoods of differential mean temperature in detected changes, and decision fusion with an infrared vacancy sensor. The proposed method is evaluated with data generated using the developed signal model as well as experimental data from a cell office/meeting room environment. We obtain an average counting error of 0.11 and 0.19 for 90% of the instants respectively when considering 15 minute windows for simulated and experimental datasets.

To compare the dose to target and organs at risk in conventional planning versus CT based 3D planning in Vaginal mound brachytherapy and to compare the effect of bladder distension on target dose distribution as well as dose to organs at risk. Patients diagnosed with carcinoma cervix or carcinoma endometrium with indication for vaginal mound brachytherapy were included in the study after a detailed gynecological assessment. All patients underwent planning CT with a full bladder and an empty bladder protocol. Target volumes and organs at risk were contoured in a planning system and brachytherapy planning was done in a brachytherapy planning system. For each CT, two plans were generated – one 2D based standard unoptimized plan and another 3D based optimized plan. Dosimetric parameters like D90, D95, V100 and V150 were reported for clinical target volume (CTV) and D0.1cc, D1cc, D2cc and D5cc were reported for organs at risk (OARs). Dosimetric comparison was done between 2D and 3D based plans and between full bladder and empty bladder protocols and the data was analyzed. 92 observations were made from data collected from 43 patients. Median age was 49 years (Range – 24 – 69). All patients had undergone hysterectomy and 54% (n = 23) of patients were diagnosed with carcinoma endometrium, followed by carcinoma cervix (30%) and carcinoma cervical stump (16%). Mean CTVsurface volume was 28.8cc (range 18.6cc– 39cc) and mean CTVdepth volume was 53cc (range 36.3cc – 68cc). Difference between CTV coverage in terms of optimized and non-optimized plans were not statistically significant for CTVsurface (p=0.286) and CTVdepth (p=0.11). Significant reduction in D0.1cc, D1cc, D2cc and D5cc dose parameters were observed in bladder, rectum, sigmoid and bowel with 3D optimized plan (p<0.001). Bladder distension did not have significant effect on CTVdepth and CTVsurface dose parameters. However, bladder distension showed a 35% reduction in dose for bowel (p<0.001) and 8% reduction in sigmoid dose which was not statistically significant (p=0.068). Bladder distension also showed a sharp 8.3% (p=0.04) increase in bladder dose correlating to the proximity of posterior bladder wall with the applicator on distension but there was a significant reduction in the mean dose to bladder. This study demonstrates the dosimetric benefits with CT based 3D planning for vaginal brachytherapy over 2D based conventional planning. 3D CT based planning helps to decrease dose to critical organs without compromising target volume coverage by individualizing the dosimetry according to each patient's anatomy. This study also illustrated the dosimetric benefits of bladder distension and kindles the need for a consensus contouring and reporting guideline for vaginal cuff brachytherapy.

Quantization, a commonly used technique to reduce the memory footprint of a neural network for edge computing, entails reducing the precision of the floating-point representation used for the parameters of the network. The impact of such rounding-off errors on the overall performance of the neural network is estimated using testing, which is not exhaustive and thus cannot be used to guarantee the safety of the model. We present a framework based on Satisfiability Modulo Theory (SMT) solvers to quantify the robustness of neural networks to parameter perturbation. To this end, we introduce notions of local and global robustness that capture the deviation in the confidence of class assignments due to parameter quantization. The robustness notions are then cast as instances of SMT problems and solved automatically using solvers, such as dReal. We demonstrate our framework on two simple Multi-Layer Perceptrons (MLP) that perform binary classification on a two-dimensional input. In addition to quantifying the robustness, we also show that Rectified Linear Unit activation results in higher robustness than linear activations for our MLPs.

We report the object-recognition performance of VGG16, ResNet, and SqueezeNet, three state-of-the-art Convolutional Neural Networks (CNNs) trained on ImageNet, across 15 different lighting conditions using the Phos dataset and a ResNet-like network trained on Pascal VOC on the ExDark dataset. The instabilities in the normalized softmax values are used to highlight that pre-trained networks are not robust to lighting variations. Our investigation yields a robustness analysis framework for analyzing the performance of CNNs under different lighting conditions. The Phos dataset consists of 15 scenes captured under different illumination conditions: 9 images captured under various strengths of uniform illumination, and 6 images under different degrees of non-uniform illumination. The ExDARK dataset consists of ten scenes under different illumination conditions. A Keras-based pipeline was developed to study the softmax values output by ImageNet-trained VGG16, ResNet, and SqueezeNet for the same object under the 15 different lighting conditions of the Phos dataset. A ResNet architecture was trained end-to-end on the PASCAL VOC dataset. Large variations observed in the softmax values provide empirical evidence of unstable performance and the need to augment training to account for lighting variations.

We present compression algorithms for analog responses of Passive Infra-Red (PIR) sensors and a corresponding benchmarking framework based on ARM Cortex-M4 micro-controller. Compression ratio, reconstruction accuracy, memory footprint, and running times for a compression algorithm based on Discrete Cosine Transform (DCT) are presented. Analog responses can be compressed by up to 90% and recovered with less than 10% error. Our framework presents a first step in overcoming the computational limitations of the edge nodes in connected lighting systems to collect fine-grained occupancy patterns and enable beyond-lighting applications, such as Space Optimization and Heating Ventilation and Air Conditioning (HVAC) controls.

This paper shows how to use Barrier Certificates (BaCs) to design Simplex Architectures for hybrid systems. The Simplex architecture entails switching control of a plant over to a provably safe Baseline Controller when a safety violation is imminent under the control of an unverified Advanced Controller. A key step of determining the switching condition is identifying a recoverable region, where the Baseline Controller guarantees recovery and keeps the plant invariably safe. BaCs, which are Lyapunov-like proofs of safety, are used to identify a recoverable region. At each time step, the switching logic samples the state of the plant and uses bounded-time reachability analysis to conservatively check whether any states outside the zero-level set of the BaCs, which therefore might be non-recoverable, are reachable in one decision period under control of the Advanced Controller. If so, failover is initiated. Our approach of using BaCs to identify recoverable states is computationally cheaper and potentially more accurate (less conservative) than existing approaches based on state-space exploration. We apply our technique to two hybrid systems: a water tank pump and a stop-sign-obeying controller for a car.

As cities ramp up the efforts to convert their aging lighting infrastructure to connected and energy-efficient Light-Emitting Diodes (LEDs), they are confounded by the lack of reliable information about their existing outdoor lighting bases. In this paper, we propose a vehicle-mounted spectrom etry-based approach to scalably audit the roadway lamp types by driving across the city, thereby quickly and efficiently providing the basis for planning and executing LED conversion projects. LambdaSeek, a mobile sensing system that can be mounted on a vehicle, is developed to reliably capture the Spectral Power Distributions (SPDs) of the light emitted by the luminaires on the light poles by driving around the city. The on-board illuminance sensor and the global positioning system receiver helps to localize the SPDs, which are then classified into the corresponding lamp types using a k-Nearest Neighbor classification algorithm. Validation experiments across four field trials are presented: the most commonly found High-Pressure Sodium, Mercury Vapor, Metal Halide and LED lamps were classified correctly with a recall rate of more than 95%.

We present BFComp, an automated framework based on Sum-Of-Squares (SOS) optimization and delta-decidability over the reals, to compute Bisimulation Functions (BFs) that characterize Input-to-Output Stability (ICS) of dynamical systems. BFs are Lyapunov-like functions that decay along the trajectories of a given pair of systems, and can be used to establish the stability of the outputs with respect to bounded input deviations.In addition to establishing IOS, BFComp is designed to provide tight bounds on the squared output errors between systems whenever possible. For this purpose, two SOS optimization formulations are employed: SOSP 1, which enforces the decay requirements-on a discretized grid over the input space, and SOSP 2, which covers the input space exhaustively. SOSP 2 is attempted first, and if the resulting error bounds are not satisfactory, SOSP 1 is used to compute a Candidate BF (CBF). The decay requirement for the BFs is then encoded as a delta-decidable formula and validated over a level set of the CBF using the dReal tool. If dReal produces a counterexample containing the states and inputs where the decay requirement is violated, this pair of vectors is used to refine the input-space grid and SOSP 1 is iterated.By computing BFs that appeal to a small-gain theorem, the BFComp framework can be used to show that a subsystem of a feedback-composed system can be replaced - with bounded error - by an approximately equivalent abstraction, thereby enabling approximate model-order reduction of dynamical systems. The BFs can then be used to obtain bounds on the error between the outputs of the original system and its reduced approximation. To this end, we illustrate the utility ofBFComp on a canonical cardiac-cell model, showing that the four-variable Markovian model for the slowly activating Potassium current I-Ks can be safely replaced by a one-variable Hodgkin-Huxley-type approximation. In addition to a detailed performance evaluation of BFComp, our case study also presents workarounds for systems with non-polynomial vector fields, which are not amenable to standard SOS optimizers. (C) 2016 Elsevier Ltd. All rights reserved.

The Internet of Things is poised to transform lighting from a simple illumination source, which is most often taken for granted, into a smart and data-rich infrastructure for the cities. To this end, we propose the Lighting-Enabled Smart City APplications and Ecosystems (LENSCAPEs) framework. LENSCAPEs involve i) city-wide wireless Outdoor Lighting Networks (OLNs), to connect the streetlights using either mesh, or cellular networks, ii) sensors, to collect heterogeneous spatio-temporal data about the city, iii) controllers, to actuate physical processes, such as lighting, and iv) other cloud-based applications, to process the data that is collected and disseminated by the city-wide wireless sensor network. Mesh-based networking technologies for OLNs, such as IEEE 802.15.4g, are evaluated by simulating network capacity and comparing with cellular technologies. Light-on-Demand (LoD), an adaptive energy-efficient lighting system based on wireless mesh networks, is presented as the primary application of small-scale OLNs. We also present a case study on a real-world deployment of LoD, which resulted in 92% energy savings over conventional luminaires.

ABSTRACTWe present BFComp, an automated framework based on Sum-Of-Squares (SOS) optimization and δ-decidability over the reals, to compute Bisimulation Functions (BFs) that characterize Input-to-Output Stability (IOS) of dynamical systems. BFs are Lyapunov-like functions that decay along the trajectories of a given pair of systems, and can be used to establish the stability of the outputs with respect to bounded input deviations. In addition to establishing IOS, BFComp is designed to provide tight bounds on the squared output errors between systems whenever possible. For this purpose, two SOS optimization formulations are employed: SOSP 1, which enforces the decay requirements on a discretized grid over the input space, and SOSP 2, which covers the input space exhaustively. SOSP 2 is attempted first, and if the resulting error bounds are not satisfactory, SOSP 1 is used to compute a Candidate BF (CBF). The decay requirement for the BFs is then encoded as a δ-decidable formula and validated over a level set of the CBF using the dReal tool. If dReal produces a counterexample containing the states and inputs where the decay requirement is violated, this pair of vectors is used to refine the input-space grid and SOSP 1 is iterated. By computing BFs that appeal to a small-gain theorem, the BFComp framework can be used to show that a subsystem of a feedback-composed system can be replaced--with bounded error--by an approximately equivalent abstraction, thereby enabling approximate model-order reduction of dynamical systems. We illustrate the utility of BFComp on a canonical cardiac-cell model, showing that the four-variable Markovian model for the slowly activating Potassium current IKs can be safely replaced by a one-variable Hodgkin-Huxley-type approximation.

By appealing to the small-gain theorem of one of the authors (Girard), we show that the 13-variable sodium-channel component of the 67-variable IMW cardiac-cell model (Iyer-Mazhari-Winslow) can be replaced by an approximately bi-similar, 2-variable HH-type (Hodgkin-Huxley) abstraction. We show that this substitution of (approximately) equals for equals is safe in the sense that the approximation error between sodium-channel models is not amplified by the feedback-loop context in which it is placed. To prove this feedback-compositionality result, we exhibit quadratic-polynomial, exponentially decaying bisimulation functions between the IMW and HH-type sodium channels, and also for the IMW-based context in which these sodium-channel models are placed. These functions allow us to quantify the overall error introduced by the sodium-channel abstraction and subsequent substitution in the IMW model. To automate computation of the bisimulation functions, we employ the SOSTOOLS optimization toolbox. Our experimental results validate our analytical findings. To the best of our knowledge, this is the first application of δ-bisimilar, feedback-assisting, compositional reasoning in biological systems.

We present the Spiral Classification Algorithm (SCA), a fast and accurate algorithm for classifying electrical spiral waves and their associated breakup in cardiac tissues. The classification performed by SCA is an essential component of the detection and analysis of various cardiac arrhythmic disorders, including ventricular tachycardia and fibrillation. Given a digitized frame of a propagating wave, SCA constructs a highly accurate representation of the front and the back of the wave, piecewise interpolates this representation with cubic splines, and subjects the result to an accurate curvature analysis. This analysis is more comprehensive than methods based on spiral-tip tracking, as it considers the entire wave front and back. To increase the smoothness of the resulting symbolic representation, the SCA uses weighted overlapping of adjacent segments which increases the smoothness at join points. SCA has been applied to a number of representative types of spiral waves, and, for each type, a distinct curvature evolution in time (signature) has been identified. Distinct signatures have also been identified for spiral breakup. These results represent a significant first step in automatically determining parameter ranges for which a computational cardiac-cell network accurately reproduces a particular kind of cardiac arrhythmia, such as ventricular fibrillation.

We show that in the context of the Iyer et al. 67-variable cardiac myocycte model (IMW), it is possible to replace the detailed 13-state probabilistic model of the sodium channel dynamics with a much simpler Hodgkin-Huxley (HH)-like two-state sodium channel model, while only incurring a bounded approximation error. The technical basis for this result is the construction of an approximate bisimulation between the HH and IMW sodium channel models, both of which are input-controlled (voltage in this case) CTMCs. The construction of the appropriate approximate bisimulation, as well as the overall result regarding the behavior of this modified IMW model, involves: (1) Identification of the voltage-dependent parameters of the m and h gates in the HH-type channel via a two-step fitting process, carried out over more than 22,000 representative observational traces of the IMW channel. (2) Proving that the distance between observations of the two channels is bounded. (3) Exploring the sensitivity of the overall IMW model to the HH-type sodium-channel approximation. Our extensive simulation results experimentally validate our findings, for varying IMW-type input stimuli.

We present the Spiral Classification Algorithm (SCA), a fast and accurate algorithm for classifying electrical spiral waves and their associated breakup in cardiac tissues. The classification performed by SCA is an essential component of the detection and analysis of various cardiac arrhythmic disorders, including ventricular tachycardia and fibrillation. Given a digitized frame of a propagating wave, SCA constructs a highly accurate representation of the front and the back of the wave, piecewise interpolates this representation with cubic splines, and subjects the result to an accurate curvature analysis. This analysis is more comprehensive than methods based on spiral-tip tracking, as it considers the entire wave front and back. To increase the smoothness of the resulting symbolic representation, the SCA uses weighted overlapping of adjacent segments which increases the smoothness at join points. SCA has been applied to several representative types of spiral waves, and for each type, a distinct curvature evolution in time (signature) has been identified. Moreover, distinguished signatures have been also identified for spiral breakup. This represents a significant first step in automatically determining parameter ranges for which a computational cardiac-cell network accurately reproduces ventricular fibrillation. The connection between parameters and physiological entities would then lead to an understanding of the root cause of the disorder and enable the development of personalized treatment strategies.

The temporal relation between the Round Trip Time (RTT) and the Congestion Window (cwnd) has been analyzed as the "chaotic relation in TCP". This relation is first justified using logical explanation. Then we devise mathematical tools to capture this relation. Then we explain the applications of capturing this chaotic relation. Internet Protocol Diagnostic Monitor (IPDM) has been used for obtaining statistics of TCP connections. This chaotic relation is expected to have widespread applications such as loss differentiators, network tuning parameters etc.

This paper proposes an LDA to help us tune a wireless network thus enabling better network utilization and throughputs, which in turn result into increased customer satisfaction. Correlation between various TCP parameters is used. CC-LDA uses a statistical approach but ensures fewer loads on a client side processing applications. Various samples were collected from the IPDM server and were analyzed. I also propose a monitoring lifecycle using CC-LDA involving a knowledge base to gain some priori knowledge through tests. The paper ends with a comparison with other existing LDAs.