Showing 1–10 of 10 results for author: Govind, R

MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm

Authors: S. Akshay, Paul Gastin, R. Govind, B. Srivathsan

Abstract: The translation of Metric Interval Temporal Logic (MITL) to timed automata is a topic that has been extensively studied. A key challenge here is the conversion of future modalities into equivalent automata. Typical conversions equip the automata with a guess-and-check mechanism to ascertain the truth of future modalities. Guess-and-check can be naturally implemented via alternation. However, since… ▽ More The translation of Metric Interval Temporal Logic (MITL) to timed automata is a topic that has been extensively studied. A key challenge here is the conversion of future modalities into equivalent automata. Typical conversions equip the automata with a guess-and-check mechanism to ascertain the truth of future modalities. Guess-and-check can be naturally implemented via alternation. However, since timed automata tools do not handle alternation, existing methods perform an additional step of converting the alternating timed automata into timed automata. This de-alternation step proceeds by an intricate finite abstraction of the space of configurations of the alternating automaton. Recently, a model of generalized timed automata (GTA) has been proposed. The model comes with several powerful additional features, and yet, the best known zone-based reachability algorithms for timed automata have been extended to the GTA model, with the same complexity for all the zone operations. We provide a new concise translation from MITL to GTA. In particular, for the timed until modality, our translation offers an exponential improvement w.r.t. the state-of-the-art. Thanks to this conversion, MITL model checking reduces to checking liveness for GTAs. However, no liveness algorithm is known for GTAs. Due to the presence of future clocks, there is no finite time-abstract bisimulation (region equivalence) for GTAs, whereas liveness algorithms for timed automata crucially rely on the presence of the finite region equivalence. As our second contribution, we provide a new zone-based algorithm for checking Buchi non-emptiness in GTAs, which circumvents this fundamental challenge. △ Less

Submitted 11 July, 2024; originally announced July 2024.

Reversible Transducers over Infinite Words

Authors: Luc Dartois, Paul Gastin, Loïc Germerie Guizouarn, R. Govind, Shankaranarayanan Krishna

Abstract: Deterministic two-way transducers capture the class of regular functions. The efficiency of composing two-way transducers has a direct implication in algorithmic problems related to reactive synthesis, where transformation specifications are converted into equivalent transducers. These specifications are presented in a modular way, and composing the resultant machines simulates the full specificat… ▽ More Deterministic two-way transducers capture the class of regular functions. The efficiency of composing two-way transducers has a direct implication in algorithmic problems related to reactive synthesis, where transformation specifications are converted into equivalent transducers. These specifications are presented in a modular way, and composing the resultant machines simulates the full specification. An important result by Dartois et al. shows that composition of two-way transducers enjoy a polynomial composition when the underlying transducer is reversible, that is, if they are both deterministic and co-deterministic. This is a major improvement over general deterministic two-way transducers, for which composition causes a doubly exponential blow-up in the size of the inputs in general. Moreover, they show that reversible two-way transducers have the same expressiveness as deterministic two-way transducers. However, the question of expressiveness of reversible transducers over infinite words is still open. In this article, we introduce the class of reversible two-way transducers over infinite words and show that they enjoy the same expressive power as deterministic two-way transducers over infinite words. This is done through a non-trivial, effective construction inducing a single exponential blow-up in the set of states. Further, we also prove that composing two reversible two-way transducers over infinite words incurs only a polynomial complexity, thereby providing foundations for efficient procedure for composition of transducers over infinite words. △ Less

Submitted 28 June, 2024; v1 submitted 17 June, 2024; originally announced June 2024.

A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation

Authors: S Akshay, Paul Gastin, R Govind, Aniruddha R Joshi, B Srivathsan

Abstract: In this paper, we consider a model of generalized timed automata (GTA) with two kinds of clocks, history and future, that can express many timed features succinctly, including timed automata, event-clock automata with and without diagonal constraints, and automata with timers. Our main contribution is a new simulation-based zone algorithm for checking reachability in this unified model. While such… ▽ More In this paper, we consider a model of generalized timed automata (GTA) with two kinds of clocks, history and future, that can express many timed features succinctly, including timed automata, event-clock automata with and without diagonal constraints, and automata with timers. Our main contribution is a new simulation-based zone algorithm for checking reachability in this unified model. While such algorithms are known to exist for timed automata, and have recently been shown for event-clock automata without diagonal constraints, this is the first result that can handle event-clock automata with diagonal constraints and automata with timers. We also provide a prototype implementation for our model and show experimental results on several benchmarks. To the best of our knowledge, this is the first effective implementation not just for our unified model, but even just for automata with timers or for event-clock automata (with predicting clocks) without going through a costly translation via timed automata. Last but not least, beyond being interesting in their own right, generalized timed automata can be used for model-checking event-clock specifications over timed automata models. △ Less

Submitted 28 May, 2023; originally announced May 2023.

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

Simulations for Event-Clock Automata

Authors: S Akshay, Paul Gastin, R Govind, B Srivathsan

Abstract: Event-clock automata (ECA) are a well-known semantic subclass of timed automata (TA) which enjoy admirable theoretical properties, e.g., determinizability, and are practically useful to capture timed specifications. However, unlike for timed automata, there exist no implementations for checking non-emptiness of event-clock automata. As ECAs contain special prophecy clocks that guess and maintain t… ▽ More Event-clock automata (ECA) are a well-known semantic subclass of timed automata (TA) which enjoy admirable theoretical properties, e.g., determinizability, and are practically useful to capture timed specifications. However, unlike for timed automata, there exist no implementations for checking non-emptiness of event-clock automata. As ECAs contain special prophecy clocks that guess and maintain the time to the next occurrence of specific events, they cannot be seen as a syntactic subclass of TA. Therefore, implementations for TA cannot be directly used for ECAs, and moreover the translation of an ECA to a semantically equivalent TA is expensive. Another reason for the lack of ECA implementations is the difficulty in adapting zone-based algorithms, critical in the timed automata setting, to the event-clock automata setting. This difficulty was studied by Geeraerts et al. in 2011, where the authors proposed a zone enumeration procedure that uses zone extrapolations for finiteness. In this article, we propose a different zone-based algorithm to solve the reachability problem for event-clock automata, using simulations for finiteness. A surprising consequence of our result is that for event-predicting automata, the subclass of event-clock automata that only use prophecy clocks, we obtain finiteness even without any simulations. For general event-clock automata, our new algorithm exploits the G-simulation framework, which is the coarsest known simulation relation in timed automata literature, and has been recently used for advances in other extensions of timed automata. △ Less

Submitted 1 July, 2024; v1 submitted 6 July, 2022; originally announced July 2022.

Efficient Construction of Reversible Transducers from Regular Transducer Expressions

Authors: Luc Dartois, Paul Gastin, R. Govind, Shankaranarayanan Krishna

Abstract: The class of regular transformations has several equivalent characterizations such as functional MSO transductions, deterministic two-way transducers, streaming string transducers, as well as regular transducer expressions (RTE). For algorithmic applications, it is very common and useful to transform a specification, here, an RTE, to a machine, here, a transducer. In this paper, we give an effic… ▽ More The class of regular transformations has several equivalent characterizations such as functional MSO transductions, deterministic two-way transducers, streaming string transducers, as well as regular transducer expressions (RTE). For algorithmic applications, it is very common and useful to transform a specification, here, an RTE, to a machine, here, a transducer. In this paper, we give an efficient construction of a two-way reversible transducer (2RFT) equivalent to a given RTE. 2RFTs are a well behaved class of transducers which are deterministic and co-deterministic (hence allows evaluation in linear time \wrt the input word), and where composition has only polynomial complexity. We show that, for full RTE, the constructed 2RFT has size doubly exponential in the size of the expression, while, if the RTE does not use Hadamard product or chained-star, the constructed 2RFT has size exponential in the size of the RTE. △ Less

Submitted 9 February, 2022; originally announced February 2022.

The side effect profile of Clozapine in real world data of three large mental hospitals

Authors: Ehtesham Iqbal, Risha Govind, Alvin Romero, Olubanke Dzahini, Matthew Broadbent, Robert Stewart, Tanya Smith, Chi-Hun Kim, Nomi Werbeloff, Richard Dobson, Zina Ibrahim

Abstract: Objective: Mining the data contained within Electronic Health Records (EHRs) can potentially generate a greater understanding of medication effects in the real world, complementing what we know from Randomised control trials (RCTs). We Propose a text mining approach to detect adverse events and medication episodes from the clinical text to enhance our understanding of adverse effects related to Cl… ▽ More Objective: Mining the data contained within Electronic Health Records (EHRs) can potentially generate a greater understanding of medication effects in the real world, complementing what we know from Randomised control trials (RCTs). We Propose a text mining approach to detect adverse events and medication episodes from the clinical text to enhance our understanding of adverse effects related to Clozapine, the most effective antipsychotic drug for the management of treatment-resistant schizophrenia, but underutilised due to concerns over its side effects. Material and Methods: We used data from de-identified EHRs of three mental health trusts in the UK (>50 million documents, over 500,000 patients, 2835 of which were prescribed Clozapine). We explored the prevalence of 33 adverse effects by age, gender, ethnicity, smoking status and admission type three months before and after the patients started Clozapine treatment. We compared the prevalence of adverse effects with those reported in the Side Effects Resource (SIDER) where possible. Results: Sedation, fatigue, agitation, dizziness, hypersalivation, weight gain, tachycardia, headache, constipation and confusion were amongst the highest recorded Clozapine adverse effect in the three months following the start of treatment. Higher percentages of all adverse effects were found in the first month of Clozapine therapy. Using a significance level of (p< 0.05) out chi-square tests show a significant association between most of the ADRs in smoking status and hospital admissions and some in gender and age groups. Further, the data was combined from three trusts, and chi-square tests were applied to estimate the average effect of ADRs in each monthly interval. Conclusion: A better understanding of how the drug works in the real world can complement clinical trials and precision medicine. △ Less

Submitted 27 January, 2020; originally announced January 2020.

PySPH: a Python-based framework for smoothed particle hydrodynamics

Authors: Prabhu Ramachandran, Aditya Bhosale, Kunal Puri, Pawan Negi, Abhinav Muta, A Dinesh, Dileep Menon, Rahul Govind, Suraj Sanka, Amal S Sebastian, Ananyo Sen, Rohan Kaushik, Anshuman Kumar, Vikas Kurapati, Mrinalgouda Patil, Deep Tavker, Pankaj Pandey, Chandrashekhar Kaushik, Arkopal Dutt, Arpit Agarwal

Abstract: PySPH is an open-source, Python-based, framework for particle methods in general and Smoothed Particle Hydrodynamics (SPH) in particular. PySPH allows a user to define a complete SPH simulation using pure Python. High-performance code is generated from this high-level Python code and executed on either multiple cores, or on GPUs, seamlessly. It also supports distributed execution using MPI. PySPH… ▽ More PySPH is an open-source, Python-based, framework for particle methods in general and Smoothed Particle Hydrodynamics (SPH) in particular. PySPH allows a user to define a complete SPH simulation using pure Python. High-performance code is generated from this high-level Python code and executed on either multiple cores, or on GPUs, seamlessly. It also supports distributed execution using MPI. PySPH supports a wide variety of SPH schemes and formulations. These include, incompressible and compressible fluid flow, elastic dynamics, rigid body dynamics, shallow water equations, and other problems. PySPH supports a variety of boundary conditions including mirror, periodic, solid wall, and inlet/outlet boundary conditions. The package is written to facilitate reuse and reproducibility. This paper discusses the overall design of PySPH and demonstrates many of its features. Several example results are shown to demonstrate the range of features that PySPH provides. △ Less

Submitted 28 December, 2020; v1 submitted 10 September, 2019; originally announced September 2019.

Comments: 39 pages, 19 figures

Journal ref: ACM Transactions on Mathematical Software, volume 47, number 4, article 34, July 2021

Revisiting local time semantics for networks of timed automata

Authors: R. Govind, Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz

Abstract: We investigate a zone based approach for the reachability problem in timed automata. The challenge is to alleviate the size explosion of the search space when considering networks of timed automata working in parallel. In the timed setting this explosion is particularly visible as even different interleavings of local actions of processes may lead to different zones. Salah et al. in 2006 have show… ▽ More We investigate a zone based approach for the reachability problem in timed automata. The challenge is to alleviate the size explosion of the search space when considering networks of timed automata working in parallel. In the timed setting this explosion is particularly visible as even different interleavings of local actions of processes may lead to different zones. Salah et al. in 2006 have shown that the union of all these different zones is also a zone. This observation was used in an algorithm which from time to time detects and aggregates these zones into a single zone. We show that such aggregated zones can be calculated more efficiently using the local time semantics and the related notion of local zones proposed by Bengtsson et al. in 1998. Next, we point out a flaw in the existing method to ensure termination of the local zone graph computation. We fix this with a new algorithm that builds the local zone graph and uses abstraction techniques over (standard) zones for termination. We evaluate our algorithm on standard examples. On various examples, we observe an order of magnitude decrease in the search space. On the other examples, the algorithm performs like the standard zone algorithm. △ Less

Submitted 4 July, 2019; originally announced July 2019.

Comments: A shorter version appears in proceedings of CONCUR 2019

MSC Class: 68Q60

Logics for Reversible Regular Languages and Semigroups with Involution

Authors: Paul Gastin, Amaldev Manuel, R. Govind

Abstract: We present MSO and FO logics with predicates `between' and `neighbour' that characterise various fragments of the class of regular languages that are closed under the reverse operation. The standard connections that exist between MSO and FO logics and varieties of finite semigroups extend to this setting with semigroups extended with an involution. The case is different for FO with neighbour relat… ▽ More We present MSO and FO logics with predicates `between' and `neighbour' that characterise various fragments of the class of regular languages that are closed under the reverse operation. The standard connections that exist between MSO and FO logics and varieties of finite semigroups extend to this setting with semigroups extended with an involution. The case is different for FO with neighbour relation where we show that one needs additional equations to characterise the class. △ Less

Submitted 2 July, 2019; originally announced July 2019.

Comments: Accepted for DLT 2019

XMCD studies of thin Co films on BaTiO$_3$

Authors: Martin Welke, Joachim Gräfe, Remya Kunjuveettil Govind, Vasili Hari Babu, Martin Trautmann, Karl-Michael Schindler, Reinhard Denecke

Abstract: Different layer thicknesses of Cobalt ranging from 2.6 Å (1.5 ML) up to 55 Å (30.5 ML) deposited on ferroelectric BaTiO$_3$ have been studied regarding their magnetic behavior. The layers have been characterized using XMCD spectroscopy at remanent magnetization. After careful data analysis the magnetic moments of the Cobalt could be determined using the sum rule formalism. There is a sudden and ab… ▽ More Different layer thicknesses of Cobalt ranging from 2.6 Å (1.5 ML) up to 55 Å (30.5 ML) deposited on ferroelectric BaTiO$_3$ have been studied regarding their magnetic behavior. The layers have been characterized using XMCD spectroscopy at remanent magnetization. After careful data analysis the magnetic moments of the Cobalt could be determined using the sum rule formalism. There is a sudden and abrupt onset in magnetism starting at thicknesses of 9 Å (5 ML) of Cobalt for measurements at 120 K and of 10 Å (5.5 ML) if measured at room temperature. Initial island growth and subsequent coalescence of Co on BaTiO$_3$ is suggested to explain the sudden onset. In that context, no magnetically dead layers are observed. △ Less

Submitted 11 August, 2015; v1 submitted 22 June, 2015; originally announced June 2015.

Comments: 9 pages, 5 figures, submitted to J. Phys. Condens. Matter

Journal ref: J. Phys.: Condens. Matter 27 326001 (2015)