Showing 1–18 of 18 results for author: Mallik, K

Efficient Dynamic Shielding for Parametric Safety Specifications

Authors: Davide Corsi, Kaushik Mallik, Andoni Rodriguez, Cesar Sanchez

Abstract: Shielding has emerged as a promising approach for ensuring safety of AI-controlled autonomous systems. The algorithmic goal is to compute a shield, which is a runtime safety enforcement tool that needs to monitor and intervene the AI controller's actions if safety could be compromised otherwise. Traditional shields are designed statically for a specific safety requirement. Therefore, if the safety… ▽ More Shielding has emerged as a promising approach for ensuring safety of AI-controlled autonomous systems. The algorithmic goal is to compute a shield, which is a runtime safety enforcement tool that needs to monitor and intervene the AI controller's actions if safety could be compromised otherwise. Traditional shields are designed statically for a specific safety requirement. Therefore, if the safety requirement changes at runtime due to changing operating conditions, the shield needs to be recomputed from scratch, causing delays that could be fatal. We introduce dynamic shields for parametric safety specifications, which are succinctly represented sets of all possible safety specifications that may be encountered at runtime. Our dynamic shields are statically designed for a given safety parameter set, and are able to dynamically adapt as the true safety specification (permissible by the parameters) is revealed at runtime. The main algorithmic novelty lies in the dynamic adaptation procedure, which is a simple and fast algorithm that utilizes known features of standard safety shields, like maximal permissiveness. We report experimental results for a robot navigation problem in unknown territories, where the safety specification evolves as new obstacles are discovered at runtime. In our experiments, the dynamic shields took a few minutes for their offline design, and took between a fraction of a second and a few seconds for online adaptation at each step, whereas the brute-force online recomputation approach was up to 5 times slower. △ Less

Submitted 28 May, 2025; originally announced May 2025.

Supermartingale Certificates for Quantitative Omega-regular Verification and Control

Authors: Thomas A. Henzinger, Kaushik Mallik, Pouya Sadeghi, Đorđe Žikelić

Abstract: We present the first supermartingale certificate for quantitative $ω$-regular properties of discrete-time infinite-state stochastic systems. Our certificate is defined on the product of the stochastic system and a limit-deterministic Büchi automaton that specifies the property of interest; hence we call it a limit-deterministic Büchi supermartingale (LDBSM). Previously known supermartingale certif… ▽ More We present the first supermartingale certificate for quantitative $ω$-regular properties of discrete-time infinite-state stochastic systems. Our certificate is defined on the product of the stochastic system and a limit-deterministic Büchi automaton that specifies the property of interest; hence we call it a limit-deterministic Büchi supermartingale (LDBSM). Previously known supermartingale certificates applied only to quantitative reachability, safety, or reach-avoid properties, and to qualitative (i.e., probability 1) $ω$-regular properties. We also present fully automated algorithms for the template-based synthesis of LDBSMs, for the case when the stochastic system dynamics and the controller can be represented in terms of polynomial inequalities. Our experiments demonstrate the ability of our method to solve verification and control tasks for stochastic systems that were beyond the reach of previous supermartingale-based approaches. △ Less

Submitted 24 May, 2025; originally announced May 2025.

Comments: Accepted at CAV 2025

Predictive Monitoring of Black-Box Dynamical Systems

Authors: Thomas A. Henzinger, Fabian Kresse, Kaushik Mallik, Emily Yu, Đorđe Žikelić

Abstract: We study the problem of predictive runtime monitoring of black-box dynamical systems with quantitative safety properties. The black-box setting stipulates that the exact semantics of the dynamical system and the controller are unknown, and that we are only able to observe the state of the controlled (aka, closed-loop) system at finitely many time points. We present a novel framework for predicting… ▽ More We study the problem of predictive runtime monitoring of black-box dynamical systems with quantitative safety properties. The black-box setting stipulates that the exact semantics of the dynamical system and the controller are unknown, and that we are only able to observe the state of the controlled (aka, closed-loop) system at finitely many time points. We present a novel framework for predicting future states of the system based on the states observed in the past. The numbers of past states and of predicted future states are parameters provided by the user. Our method is based on a combination of Taylor's expansion and the backward difference operator for numerical differentiation. We also derive an upper bound on the prediction error under the assumption that the system dynamics and the controller are smooth. The predicted states are then used to predict safety violations ahead in time. Our experiments demonstrate practical applicability of our method for complex black-box systems, showing that it is computationally lightweight and yet significantly more accurate than the state-of-the-art predictive safety monitoring techniques. △ Less

Submitted 21 December, 2024; originally announced December 2024.

Comments: Submitted to L4DC 2025

New Insights Into Achievable Spectral Efficiency With Adaptive Free Space Optical Transmissions

Authors: Himani Verma, Kamal Singh, Ranjan K. Mallik

Abstract: Terrestrial free-space optical (FSO) communication systems, while designed to operate on large unlicensed optical bandwidths, are power-constrained due to strict eye safety regulations. The channel fluctuation inherent in terrestrial FSO links also limits the received optical power. Consequently, the available signal-to-noise ratio (SNR) per Hz could become limited; this holds for future long-haul… ▽ More Terrestrial free-space optical (FSO) communication systems, while designed to operate on large unlicensed optical bandwidths, are power-constrained due to strict eye safety regulations. The channel fluctuation inherent in terrestrial FSO links also limits the received optical power. Consequently, the available signal-to-noise ratio (SNR) per Hz could become limited; this holds for future long-haul terrestrial systems based on coherent optical communications. An efficient and adaptive transmission mechanism is thus crucial at the optical source. However, a critical assessment of the impact of adaptive transmission in terrestrial FSO systems has received less attention in the literature. This work studies terrestrial FSO communication systems employing adaptive beam transmission while detection receivers operate under shot noise-limited conditions. Specifically, we propose a novel exact closed-form expression for the average spectral efficiency of these FSO systems with transmit beam power adaptation over the gamma-gamma turbulence channel with pointing error. More importantly, we provide a detailed assessment of the impact of turbulence and pointing error impairments on the performance of the aforementioned FSO systems, revealing several novel and counterintuitive insights. In particular, the extensive numerical results help elucidate the intricacies of analyzing these terrestrial FSO systems and clarify a few misconceptions alluded to in recent related literature. △ Less

Submitted 12 May, 2025; v1 submitted 17 February, 2024; originally announced February 2024.

An Efficient Ratio Detector for Ambient Backscatter Communication

Authors: Wenjing Liu, Shanpu Shen, Danny H. K. Tsang, Ranjan K. Mallik, Ross Murch

Abstract: Ambient backscatter communication (AmBC) leverages the existing ambient radio frequency (RF) environment to implement communication with battery-free devices. One critical challenge of AmBC systems is signal recovery because the transmitted information bits are embedded in the ambient RF signals and these are unknown and uncontrollable. To address this problem, most existing approaches use averagi… ▽ More Ambient backscatter communication (AmBC) leverages the existing ambient radio frequency (RF) environment to implement communication with battery-free devices. One critical challenge of AmBC systems is signal recovery because the transmitted information bits are embedded in the ambient RF signals and these are unknown and uncontrollable. To address this problem, most existing approaches use averaging-based energy detectors and consequently the data rate is low and there is an error floor. Here we propose a new detection strategy based on the ratio between signals received from a multiple-antenna Reader. The advantage of using the ratio is that ambient RF signals are removed directly from the embedded signals without averaging and hence it can increase data rates and avoid the error floor. Different from original ratio detectors that use the magnitude ratio of the signals between two Reader antennas, in our proposed approach, we utilize the complex ratio so that phase information is preserved and propose an accurate linear channel model approximation. This allows the application of existing linear detection techniques from which we can obtain a minimum distance detector and closed-form expressions for bit error rate (BER). In addition, averaging, coding and interleaving can also be included to further enhance the BER. The results are also general, allowing any number of Reader antennas to be utilized in the approach. Numerical results demonstrate that the proposed approach performs better than approaches based on energy detection and original ratio detectors. △ Less

Submitted 18 October, 2022; originally announced October 2022.

Fast Symbolic Algorithms for Omega-Regular Games under Strong Transition Fairness

Authors: Tamajit Banerjee, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, Sadegh Soudjani

Abstract: We consider fixpoint algorithms for two-player games on graphs with $ω$-regular winning conditions, where the environment is constrained by a strong transition fairness assumption. Strong transition fairness is a widely occurring special case of strong fairness, which requires that any execution is strongly fair with respect to a specified set of live edges: whenever the source vertex of a live ed… ▽ More We consider fixpoint algorithms for two-player games on graphs with $ω$-regular winning conditions, where the environment is constrained by a strong transition fairness assumption. Strong transition fairness is a widely occurring special case of strong fairness, which requires that any execution is strongly fair with respect to a specified set of live edges: whenever the source vertex of a live edge is visited infinitely often along a play, the edge itself is traversed infinitely often along the play as well. We show that, surprisingly, strong transition fairness retains the algorithmic characteristics of the fixpoint algorithms for $ω$-regular games -- the new algorithms have the same alternation depth as the classical algorithms but invoke a new type of predecessor operator. For Rabin games with $k$ pairs, the complexity of the new algorithm is $O(n^{k+2}k!)$ symbolic steps, which is independent of the number of live edges in the strong transition fairness assumption. Further, we show that GR(1) specifications with strong transition fairness assumptions can be solved with a 3-nested fixpoint algorithm, same as the usual algorithm. In contrast, strong fairness necessarily requires increasing the alternation depth depending on the number of fairness assumptions. We get symbolic algorithms for (generalized) Rabin, parity and GR(1) objectives under strong transition fairness assumptions as well as a direct symbolic algorithm for qualitative winning in stochastic $ω$-regular games that runs in $O(n^{k+2}k!)$ symbolic steps, improving the state of the art. Finally, we have implemented a BDD-based synthesis engine based on our algorithm. We show on a set of synthetic and real benchmarks that our algorithm is scalable, parallelizable, and outperforms previous algorithms by orders of magnitude. △ Less

Submitted 23 February, 2023; v1 submitted 15 February, 2022; originally announced February 2022.

Journal ref: TheoretiCS, Volume 2 (February 24, 2023) theoretics:9088

Machine Learning Based Parameter Estimation of Gaussian Quantum States

Authors: Neel Kanth Kundu, Matthew R. McKay, Ranjan K. Mallik

Abstract: We propose a machine learning framework for parameter estimation of single mode Gaussian quantum states. Under a Bayesian framework, our approach estimates parameters of suitable prior distributions from measured data. For phase-space displacement and squeezing parameter estimation, this is achieved by introducing Expectation-Maximization (EM) based algorithms, while for phase parameter estimation… ▽ More We propose a machine learning framework for parameter estimation of single mode Gaussian quantum states. Under a Bayesian framework, our approach estimates parameters of suitable prior distributions from measured data. For phase-space displacement and squeezing parameter estimation, this is achieved by introducing Expectation-Maximization (EM) based algorithms, while for phase parameter estimation an empirical Bayes method is applied. The estimated prior distribution parameters along with the observed data are used for finding the optimal Bayesian estimate of the unknown displacement, squeezing and phase parameters. Our simulation results show that the proposed algorithms have estimation performance that is very close to that of Genie Aided Bayesian estimators, that assume perfect knowledge of the prior parameters. Our proposed methods can be utilized by experimentalists to find the optimum Bayesian estimate of parameters of Gaussian quantum states by using only the observed measurements without requiring any knowledge about the prior distribution parameters. △ Less

Submitted 13 August, 2021; originally announced August 2021.

Comments: Submitted to IEEE Transactions on Quantum Engineering

MIMO Terahertz Quantum Key Distribution

Authors: Neel Kanth Kundu, Soumya P. Dash, Matthew R. McKay, Ranjan K. Mallik

Abstract: We propose a multiple-input multiple-output (MIMO) quantum key distribution (QKD) scheme for terahertz (THz) frequency applications operating at room temperature. Motivated by classical MIMO communications, a transmit-receive beamforming scheme is proposed that converts the rank-$r$ MIMO channel between Alice and Bob into $r$ parallel lossy quantum channels. Compared with existing single-antenna Q… ▽ More We propose a multiple-input multiple-output (MIMO) quantum key distribution (QKD) scheme for terahertz (THz) frequency applications operating at room temperature. Motivated by classical MIMO communications, a transmit-receive beamforming scheme is proposed that converts the rank-$r$ MIMO channel between Alice and Bob into $r$ parallel lossy quantum channels. Compared with existing single-antenna QKD schemes, we demonstrate that the MIMO QKD scheme leads to performance improvements by increasing the secret key rate and extending the transmission distance. Our simulation results show that multiple antennas are necessary to overcome the high free-space path loss at THz frequencies. We demonstrate a non-monotonic relation between performance and frequency, and reveal that positive key rates are achievable in the $10-30$ THz frequency range. The proposed scheme can be used for both indoor and outdoor QKD applications for beyond fifth-generation ultra-secure wireless communications systems. △ Less

Submitted 10 July, 2021; v1 submitted 8 May, 2021; originally announced May 2021.

Comments: Revisions submitted to IEEE Communications Letters

Incremental Relaying for Power Line Communication: Performance Analysis and Power Allocation

Authors: Ankit Dubey, Chinmoy Kundu, Telex M. N. Ngatched, Octavia A. Dobre, Ranjan K. Mallik

Abstract: In this paper, incremental decode-and-forward (IDF) and incremental selective decode-and-forward (ISDF) relaying are proposed to improve the spectral efficiency of power line communication. Contrary to the traditional decode-and-forward (DF) relaying, IDF and ISDF strategies utilize the relay only if the direct link ceases to attain a certain information rate, thereby improving the spectral effici… ▽ More In this paper, incremental decode-and-forward (IDF) and incremental selective decode-and-forward (ISDF) relaying are proposed to improve the spectral efficiency of power line communication. Contrary to the traditional decode-and-forward (DF) relaying, IDF and ISDF strategies utilize the relay only if the direct link ceases to attain a certain information rate, thereby improving the spectral efficiency. The path gain through the power line is assumed to be log-normally distributed with high distance-dependent attenuation and the additive noise is from a Bernoulli-Gaussian process. Closed-form expressions for the outage probability, and approximate closed-form expressions for the end-to-end average channel capacity and the average bit error rate for binary phase-shift keying are derived. Furthermore, a closed-form expression for the fraction of times the relay is in use is derived as a measure of the spectral efficiency. Comparative analysis of IDF and ISDF with traditional DF relaying is presented. It is shown that IDF is a specific case of ISDF and can obtain optimal spectral efficiency without compromising the outage performance. By employing power allocation to minimize the outage probability, it is realized that the power should be allocated in accordance with the inter-node distances and channel parameters. △ Less

Submitted 9 March, 2021; originally announced March 2021.

Symbolic Control for Stochastic Systems via Finite Parity Games

Authors: Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, Sadegh Soudjani

Abstract: We consider the problem of computing the maximal probability of satisfying an omega-regular specification for stochastic nonlinear systems evolving in discrete time. The problem reduces, after automata-theoretic constructions, to finding the maximal probability of satisfying a parity condition on a (possibly hybrid) state space. While characterizing the exact satisfaction probability is open, we s… ▽ More We consider the problem of computing the maximal probability of satisfying an omega-regular specification for stochastic nonlinear systems evolving in discrete time. The problem reduces, after automata-theoretic constructions, to finding the maximal probability of satisfying a parity condition on a (possibly hybrid) state space. While characterizing the exact satisfaction probability is open, we show that a lower bound on this probability can be obtained by (I) computing an under-approximation of the qualitative winning region, i.e., states from which the parity condition can be enforced almost surely, and (II) computing the maximal probability of reaching this qualitative winning region. The heart of our approach is a technique to symbolically compute the under-approximation of the qualitative winning region in step (I) via a finite-state abstraction of the original system as a 2.5-player parity game. Our abstraction procedure uses only the support of the probabilistic evolution; it does not use precise numerical transition probabilities. We prove that the winning set in the abstract 2.5-player game induces an under-approximation of the qualitative winning region in the original synthesis problem, along with a policy to solve it. By combining these contributions with (a) a symbolic fixpoint algorithm to solve 2.5-player games and (b) existing techniques for reachability policy synthesis in stochastic nonlinear systems, we get an abstraction-based algorithm for finding a lower bound on the maximal satisfaction probability. We have implemented the abstraction-based algorithm in Mascot-SDS (Majumdar et al., 2020), where we combined the outlined abstraction step with our recent tool FairSyn. We evaluated our implementation on the nonlinear model of a perturbed bistable switch from the literature. We outperform a recently proposed tool for solving this problem by a large margin. △ Less

Submitted 29 September, 2022; v1 submitted 4 January, 2021; originally announced January 2021.

Comments: 54 pages, under review in the Elsevier journal of Nonlinear Analysis: Hybrid Systems

ACM Class: G.3; I.1.2; I.1.4

RACH in Self-Powered NB-IoT Networks: Energy Availability and Performance Evaluation

Authors: Yan Liu, Yansha Deng, Maged Elkashlan, Arumugam Nallanathan, Jinhong Yuan, Ranjan K. Mallik

Abstract: NarrowBand-Internet of Things (NB-IoT) is a new 3GPP radio access technology designed to provide better coverage for a massive number of low-throughput low-cost devices in delay-tolerant applications with low power consumption. To provide reliable connections with extended coverage, a repetition transmission scheme is introduced to NB-IoT during both Random Access CHannel (RACH) procedure and data… ▽ More NarrowBand-Internet of Things (NB-IoT) is a new 3GPP radio access technology designed to provide better coverage for a massive number of low-throughput low-cost devices in delay-tolerant applications with low power consumption. To provide reliable connections with extended coverage, a repetition transmission scheme is introduced to NB-IoT during both Random Access CHannel (RACH) procedure and data transmission procedure. To avoid the difficulty in replacing the battery for IoT devices, the energy harvesting is considered as a promising solution to support energy sustainability in the NB-IoT network. In this work, we analyze RACH success probability in a self-powered NB-IoT network taking into account the repeated preamble transmissions and collisions, where each IoT device with data is active when its battery energy is sufficient to support the transmission. We model the temporal dynamics of the energy level as a birth-death process, derive the energy availability of each IoT device, and examine its dependence on the energy storage capacity and the repetition value. We show that in certain scenarios, the energy availability remains unchanged despite randomness in the energy harvesting. We also derive the exact expression for the RACH success probability of a {randomly chosen} IoT device under the derived energy availability, which is validated under different repetition values via simulations. We show that the repetition scheme can efficiently improve the RACH success probability in a light traffic scenario, but only slightly improves that performance with very inefficient channel resource utilization in a heavy traffic scenario. △ Less

Submitted 23 November, 2020; originally announced November 2020.

Comments: 14 pages, 13 figures, Accepted in IEEE TCOM

Resilient Abstraction-Based Controller Design

Authors: Stanly Samuel, Kaushik Mallik, Anne-Kathrin Schmuck, Daniel Neider

Abstract: We consider the computation of resilient controllers for perturbed non-linear dynamical systems w.r.t. linear-time temporal logic specifications. We address this problem through the paradigm of Abstraction-Based Controller Design (ABCD) where a finite state abstraction of the perturbed system dynamics is constructed and utilized for controller synthesis. In this context, our contribution is twofol… ▽ More We consider the computation of resilient controllers for perturbed non-linear dynamical systems w.r.t. linear-time temporal logic specifications. We address this problem through the paradigm of Abstraction-Based Controller Design (ABCD) where a finite state abstraction of the perturbed system dynamics is constructed and utilized for controller synthesis. In this context, our contribution is twofold: (I) We construct abstractions which model the impact of occasional high disturbance spikes on the system via so called disturbance edges. (II) We show that the application of resilient reactive synthesis techniques to these abstract models results in closed loop systems which are optimally resilient to these occasional high disturbance spikes. We have implemented this resilient ABCD workflow on top of SCOTS and showcase our method through multiple robot planning examples. △ Less

Submitted 14 August, 2020; originally announced August 2020.

Comments: 9 pages, 5 images, 1 table, to appear in CDC 2020

Symbolic Controller Synthesis for Büchi Specifications on Stochastic Systems

Authors: Rupak Majumdar, Kaushik Mallik, Sadegh Soudjani

Abstract: We consider the policy synthesis problem for continuous-state controlled Markov processes evolving in discrete time, when the specification is given as a Büchi condition (visit a set of states infinitely often). We decompose computation of the maximal probability of satisfying the Büchi condition into two steps. The first step is to compute the maximal qualitative winning set, from where the Büchi… ▽ More We consider the policy synthesis problem for continuous-state controlled Markov processes evolving in discrete time, when the specification is given as a Büchi condition (visit a set of states infinitely often). We decompose computation of the maximal probability of satisfying the Büchi condition into two steps. The first step is to compute the maximal qualitative winning set, from where the Büchi condition can be enforced with probability one. The second step is to find the maximal probability of reaching the already computed qualitative winning set. In contrast with finite-state models, we show that such a computation only gives a lower bound on the maximal probability where the gap can be non-zero. In this paper we focus on approximating the qualitative winning set, while pointing out that the existing approaches for unbounded reachability computation can solve the second step. We provide an abstraction-based technique to approximate the qualitative winning set by simultaneously using an over- and under-approximation of the probabilistic transition relation. Since we are interested in qualitative properties, the abstraction is non-probabilistic; instead, the probabilistic transitions are assumed to be under the control of a (fair) adversary. Thus, we reduce the original policy synthesis problem to a Büchi game under a fairness assumption and characterize upper and lower bounds on winning sets as nested fixed point expressions in the $μ$-calculus. This characterization immediately provides a symbolic algorithm scheme. Further, a winning strategy computed on the abstract game can be refined to a policy on the controlled Markov process. We describe a concrete abstraction procedure and demonstrate our algorithm on two case studies. △ Less

Submitted 14 February, 2020; v1 submitted 26 October, 2019; originally announced October 2019.

Journal ref: 23rd ACM International Conference on Hybrid Systems: Computation and Control (HSCC '20), April 22--24, 2020, Sydney, NSW, Australia

Lazy Abstraction-Based Controller Synthesis

Authors: Kyle Hsu, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck

Abstract: We present lazy abstraction-based controller synthesis (ABCS) for continuous-time nonlinear dynamical systems against reach-avoid and safety specifications. State-of-the-art multi-layered ABCS pre-computes multiple finite-state abstractions of varying granularity and applies reactive synthesis to the coarsest abstraction whenever feasible, but adaptively considers finer abstractions when necessary… ▽ More We present lazy abstraction-based controller synthesis (ABCS) for continuous-time nonlinear dynamical systems against reach-avoid and safety specifications. State-of-the-art multi-layered ABCS pre-computes multiple finite-state abstractions of varying granularity and applies reactive synthesis to the coarsest abstraction whenever feasible, but adaptively considers finer abstractions when necessary. Lazy ABCS improves this technique by constructing abstractions on demand. Our insight is that the abstract transition relation only needs to be locally computed for a small set of frontier states at the precision currently required by the synthesis algorithm. We show that lazy ABCS can significantly outperform previous multi-layered ABCS algorithms: on standard benchmarks, lazy ABCS is more than 4 times faster. △ Less

Submitted 9 August, 2019; v1 submitted 8 April, 2018; originally announced April 2018.

Lazy Abstraction-Based Control for Safety Specifications

Authors: Kyle Hsu, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck

Abstract: We present a lazy version of multi-layered abstraction-based controller synthesis (ABCS) for continuous-time nonlinear dynamical systems against safety specifications. State-of-the-art multi-layered ABCS uses pre-computed finite-state abstractions of different coarseness. Our new algorithm improves this technique by computing transitions on-the-fly, and only when a particular region of the state s… ▽ More We present a lazy version of multi-layered abstraction-based controller synthesis (ABCS) for continuous-time nonlinear dynamical systems against safety specifications. State-of-the-art multi-layered ABCS uses pre-computed finite-state abstractions of different coarseness. Our new algorithm improves this technique by computing transitions on-the-fly, and only when a particular region of the state space needs to be explored by the controller synthesis algorithm for a specific coarseness. Additionally, our algorithm improves upon existing techniques by using coarser cells on a larger subset of the state space, which leads to significant computational savings. △ Less

Submitted 26 July, 2019; v1 submitted 8 April, 2018; originally announced April 2018.

Comments: CDC 2018 camera-ready. 6 pages, 3 figures

Incremental selective decode-and-forward relaying for power line communication

Authors: A. Dubey, C. Kundu, T. M. N. Ngatched, O. A. Dobre, R. K. Mallik

Abstract: In this paper, an incremental selective decode-and-forward (ISDF) relay strategy is proposed for power line communication (PLC) systems to improve the spectral efficiency. Traditional decode-and-forward (DF) relaying employs two time slots by using half-duplex relays which significantly reduces the spectral efficiency. The ISDF strategy utilizes the relay only if the direct link quality fails to a… ▽ More In this paper, an incremental selective decode-and-forward (ISDF) relay strategy is proposed for power line communication (PLC) systems to improve the spectral efficiency. Traditional decode-and-forward (DF) relaying employs two time slots by using half-duplex relays which significantly reduces the spectral efficiency. The ISDF strategy utilizes the relay only if the direct link quality fails to attain a certain information rate, thereby improving the spectral efficiency. The path gain is assumed to be log-normally distributed with very high distance dependent signal attenuation. Furthermore, the additive noise is modeled as a Bernoulli-Gaussian process to incorporate the effects of impulsive noise contents. Closed-form expressions for the outage probability and the fraction of times the relay is in use, and an approximate closed-form expression for the average bit error rate (BER) are derived for the binary phase-shift keying signaling scheme. We observe that the fraction of times the relay is in use can be significantly reduced compared to the traditional DF strategy. It is also observed that at high transmit power, the spectral efficiency increases while the average BER decreases with increase in the required rate. △ Less

Submitted 1 March, 2018; originally announced March 2018.

Comments: 6 pages, 4 figures, VTC Fall 2017

Compositional Construction of Finite State Abstractions for Stochastic Control Systems

Authors: Kaushik Mallik, Sadegh Esmaeil Zadeh Soudjani, Anne-Kathrin Schmuck, Rupak Majumdar

Abstract: Controller synthesis techniques for continuous systems with respect to temporal logic specifications typically use a finite-state symbolic abstraction of the system. Constructing this abstraction for the entire system is computationally expensive, and does not exploit natural decompositions of many systems into interacting components. We have recently introduced a new relation, called (approximate… ▽ More Controller synthesis techniques for continuous systems with respect to temporal logic specifications typically use a finite-state symbolic abstraction of the system. Constructing this abstraction for the entire system is computationally expensive, and does not exploit natural decompositions of many systems into interacting components. We have recently introduced a new relation, called (approximate) disturbance bisimulation for compositional symbolic abstraction to help scale controller synthesis for temporal logic to larger systems. In this paper, we extend the results to stochastic control systems modeled by stochastic differential equations. Given any stochastic control system satisfying a stochastic version of the incremental input-to-state stability property and a positive error bound, we show how to construct a finite-state transition system (if there exists one) which is disturbance bisimilar to the given stochastic control system. Given a network of stochastic control systems, we give conditions on the simultaneous existence of disturbance bisimilar abstractions to every component allowing for compositional abstraction of the network system. △ Less

Submitted 27 September, 2017; originally announced September 2017.

Comments: This paper has been accepted for publication in CDC 2017

Compositional Abstraction-Based Controller Synthesis for Continuous-Time Systems

Authors: Kaushik Mallik, Anne-Kathrin Schmuck, Sadegh Soudjani, Rupak Majumdar

Abstract: Controller synthesis techniques for continuous systems with respect to temporal logic specifications typically use a finite-state symbolic abstraction of the system model. Constructing this abstraction for the entire system is computationally expensive, and does not exploit natural decompositions of many systems into interacting components. We describe a methodology for compositional symbolic abst… ▽ More Controller synthesis techniques for continuous systems with respect to temporal logic specifications typically use a finite-state symbolic abstraction of the system model. Constructing this abstraction for the entire system is computationally expensive, and does not exploit natural decompositions of many systems into interacting components. We describe a methodology for compositional symbolic abstraction to help scale controller synthesis for temporal logic to larger systems. We introduce a new relation, called (approximate) disturbance bisimulation, as the basis for compositional symbolic abstractions. Disturbance bisimulation strengthens the standard approximate alternating bisimulation relation used in control. It extends naturally to systems which are composed of weakly interconnected sub-components possibly connected in feedback, and models the coupling signals as disturbances. After proving this composability of disturbance bisimulation for metric systems we apply this result to the compositional abstraction of networks of input-to-state stable deterministic non-linear control systems. We give conditions that allow to construct finite-state abstractions compositionally for each component in such a network, so that the abstractions are simultaneously disturbance bisimilar to their continuous counterparts. Combining these two results, we show conditions under which one can compositionally abstract a network of non-linear control systems in a modular way while ensuring that the final composed abstraction is disturbance bisimilar to the original system. We discuss how we get a compositional abstraction-based controller synthesis methodology for networks of such systems against local temporal specifications as a by-product of our construction. △ Less

Submitted 9 August, 2017; v1 submitted 27 December, 2016; originally announced December 2016.