-
On Naisargik Images of Varshamov-Tenengolts and Helberg Codes
Authors:
Kalp Pandya,
Devdeep Shetranjiwala,
Naisargi Savaliya,
Manish K. Gupta
Abstract:
The VT and Helberg codes, both in binary and non-binary forms, stand as elegant solutions for rectifying insertion and deletion errors. In this paper we consider the quaternary versions of these codes. It is well known that many optimal binary non-linear codes like Kerdock and Prepreta can be depicted as Gray images (isometry) of codes defined over $\mathbb{Z}_4$. Thus a natural question arises: C…
▽ More
The VT and Helberg codes, both in binary and non-binary forms, stand as elegant solutions for rectifying insertion and deletion errors. In this paper we consider the quaternary versions of these codes. It is well known that many optimal binary non-linear codes like Kerdock and Prepreta can be depicted as Gray images (isometry) of codes defined over $\mathbb{Z}_4$. Thus a natural question arises: Can we find similar maps between quaternary and binary spaces which gives interesting properties when applied to the VT and Helberg codes. We found several such maps called Naisargik (natural) maps and we study the images of quaternary VT and Helberg codes under these maps. Naisargik and inverse Naisargik images gives interesting error-correcting properties for VT and Helberg codes. If two Naisargik images of VT code generates an intersecting one deletion sphere, then the images holds the same weights. A quaternary Helberg code designed to correct $s$ deletions can effectively rectify $s+1$ deletion errors when considering its Naisargik image, and $s$-deletion correcting binary Helberg code can corrects $\lfloor\frac{s}{2}\rfloor$ errors with inverse Naisargik image.
△ Less
Submitted 11 April, 2024;
originally announced April 2024.
-
PEFT-MedAware: Large Language Model for Medical Awareness
Authors:
Keivalya Pandya
Abstract:
Chat models are capable of answering a wide range of questions, however, the accuracy of their responses is highly uncertain. In this research, we propose a specialized PEFT-MedAware model where we utilize parameter-efficient fine-tuning (PEFT) to enhance the Falcon-1b large language model on specialized MedQuAD data consisting of 16,407 medical QA pairs, leveraging only 0.44% of its trainable par…
▽ More
Chat models are capable of answering a wide range of questions, however, the accuracy of their responses is highly uncertain. In this research, we propose a specialized PEFT-MedAware model where we utilize parameter-efficient fine-tuning (PEFT) to enhance the Falcon-1b large language model on specialized MedQuAD data consisting of 16,407 medical QA pairs, leveraging only 0.44% of its trainable parameters to enhance computational efficiency. The paper adopts data preprocessing and PEFT to optimize model performance, complemented by a BitsAndBytesConfig for efficient transformer training. The resulting model was capable of outperforming other LLMs in medical question-answering tasks in specific domains with greater accuracy utilizing limited computational resources making it suitable for deployment in resource-constrained environments. We propose further improvements through expanded datasets, larger models, and feedback mechanisms for sustained medical relevancy. Our work highlights the efficiency gains and specialized capabilities of PEFT in medical AI, outpacing standard models in precision without extensive resource demands. The proposed model and data are released for research purposes only.
△ Less
Submitted 17 November, 2023;
originally announced November 2023.
-
Automating Customer Service using LangChain: Building custom open-source GPT Chatbot for organizations
Authors:
Keivalya Pandya,
Mehfuza Holia
Abstract:
In the digital age, the dynamics of customer service are evolving, driven by technological advancements and the integration of Large Language Models (LLMs). This research paper introduces a groundbreaking approach to automating customer service using LangChain, a custom LLM tailored for organizations. The paper explores the obsolescence of traditional customer support techniques, particularly Freq…
▽ More
In the digital age, the dynamics of customer service are evolving, driven by technological advancements and the integration of Large Language Models (LLMs). This research paper introduces a groundbreaking approach to automating customer service using LangChain, a custom LLM tailored for organizations. The paper explores the obsolescence of traditional customer support techniques, particularly Frequently Asked Questions (FAQs), and proposes a paradigm shift towards responsive, context-aware, and personalized customer interactions. The heart of this innovation lies in the fusion of open-source methodologies, web scra**, fine-tuning, and the seamless integration of LangChain into customer service platforms. This open-source state-of-the-art framework, presented as "Sahaay," demonstrates the ability to scale across industries and organizations, offering real-time support and query resolution. Key elements of this research encompass data collection via web scra**, the role of embeddings, the utilization of Google's Flan T5 XXL, Base and Small language models for knowledge retrieval, and the integration of the chatbot into customer service platforms. The results section provides insights into their performance and use cases, here particularly within an educational institution. This research heralds a new era in customer service, where technology is harnessed to create efficient, personalized, and responsive interactions. Sahaay, powered by LangChain, redefines the customer-company relationship, elevating customer retention, value extraction, and brand image. As organizations embrace LLMs, customer service becomes a dynamic and customer-centric ecosystem.
△ Less
Submitted 9 October, 2023;
originally announced October 2023.
-
Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete
Authors:
Shankara Narayanan Krishna,
Khushraj Nanik Madnani,
Rupak Majumdar,
Paritosh K. Pandya
Abstract:
We investigate the decidability of the ${0,\infty}$ fragment of Timed Propositional Temporal Logic (TPTL). We show that the satisfiability checking of TPTL$^{0,\infty}$ is PSPACE-complete. Moreover, even its 1-variable fragment (1-TPTL$^{0,\infty}$) is strictly more expressive than Metric Interval Temporal Logic (MITL) for which satisfiability checking is EXPSPACE complete. Hence, we have a strict…
▽ More
We investigate the decidability of the ${0,\infty}$ fragment of Timed Propositional Temporal Logic (TPTL). We show that the satisfiability checking of TPTL$^{0,\infty}$ is PSPACE-complete. Moreover, even its 1-variable fragment (1-TPTL$^{0,\infty}$) is strictly more expressive than Metric Interval Temporal Logic (MITL) for which satisfiability checking is EXPSPACE complete. Hence, we have a strictly more expressive logic with computationally easier satisfiability checking. To the best of our knowledge, TPTL$^{0,\infty}$ is the first multi-variable fragment of TPTL for which satisfiability checking is decidable without imposing any bounds/restrictions on the timed words (e.g. bounded variability, bounded time, etc.). The membership in PSPACE is obtained by a reduction to the emptiness checking problem for a new "non-punctual" subclass of Alternating Timed Automata with multiple clocks called Unilateral Very Weak Alternating Timed Automata (VWATA$^{0,\infty}$) which we prove to be in PSPACE. We show this by constructing a simulation equivalent non-deterministic timed automata whose number of clocks is polynomial in the size of the given VWATA$^{0,\infty}$.
△ Less
Submitted 1 September, 2023;
originally announced September 2023.
-
A Review on Quantum Approximate Optimization Algorithm and its Variants
Authors:
Kostas Blekos,
Dean Brand,
Andrea Ceschini,
Chiao-Hui Chou,
Rui-Hao Li,
Komal Pandya,
Alessandro Summer
Abstract:
The Quantum Approximate Optimization Algorithm (QAOA) is a highly promising variational quantum algorithm that aims to solve combinatorial optimization problems that are classically intractable. This comprehensive review offers an overview of the current state of QAOA, encompassing its performance analysis in diverse scenarios, its applicability across various problem instances, and considerations…
▽ More
The Quantum Approximate Optimization Algorithm (QAOA) is a highly promising variational quantum algorithm that aims to solve combinatorial optimization problems that are classically intractable. This comprehensive review offers an overview of the current state of QAOA, encompassing its performance analysis in diverse scenarios, its applicability across various problem instances, and considerations of hardware-specific challenges such as error susceptibility and noise resilience. Additionally, we conduct a comparative study of selected QAOA extensions and variants, while exploring future prospects and directions for the algorithm. We aim to provide insights into key questions about the algorithm, such as whether it can outperform classical algorithms and under what circumstances it should be used. Towards this goal, we offer specific practical points in a form of a short guide. Keywords: Quantum Approximate Optimization Algorithm (QAOA), Variational Quantum Algorithms (VQAs), Quantum Optimization, Combinatorial Optimization Problems, NISQ Algorithms
△ Less
Submitted 26 June, 2023; v1 submitted 15 June, 2023;
originally announced June 2023.
-
Logics Meet 2-Way 1-Clock Alternating Timed Automata
Authors:
Shankara Narayanan Krishna,
Khushraj Nanik Madnani,
Manuel Mazo Jr.,
Paritosh K. Pandya
Abstract:
In this paper, we study the extension of 1-clock Alternating Timed Automata (1-ATA) with the ability to read in both forward and backward direction, the 2-Way 1-clock Alternating Timed Automata (2-Way 1-ATA). We show that subclass of 2-Way 1-ATA with reset free loops (2-Way 1-ATA-rfl) is expressively equivalent to MSO[<] extended with Guarded Metric Quantifiers (GQMSO). Emptiness Checking problem…
▽ More
In this paper, we study the extension of 1-clock Alternating Timed Automata (1-ATA) with the ability to read in both forward and backward direction, the 2-Way 1-clock Alternating Timed Automata (2-Way 1-ATA). We show that subclass of 2-Way 1-ATA with reset free loops (2-Way 1-ATA-rfl) is expressively equivalent to MSO[<] extended with Guarded Metric Quantifiers (GQMSO). Emptiness Checking problem for 2-Way 1-ATA-rfl (and hence GQMSO) is undecidable, in general. We propose a "non-punctuality" like restriction, called non-adjacency, for 2-Way 1-ATA-rfl, and also for GQMSO, for which the emptiness (respectively, satisfiability) checking becomes decidable. Non-Adjacent 2-Way 1-ATA is the first such class of Timed Automata with alternations and 2-wayness for which the emptiness checking is decidable (and that too with elementary complexity). We also show that 2-Way 1-ATA-rfl, even with the non-adjacent restrictions, can express properties is not recognizable using 1-ATA.
△ Less
Submitted 26 February, 2022; v1 submitted 27 July, 2021;
originally announced July 2021.
-
ReQuBiS -- Reconfigurable Quadrupedal-Bipedal Snake Robots
Authors:
Harshad Zade,
Aadesh Varude,
Karan Pandya,
A**kya Kamat,
Shital Chiddarwar,
Rohan Thakker
Abstract:
The selection of mobility modes for robot navigation consists of various trade-offs. Snake robots are ideal for traversing through constrained environments such as pipes, cluttered and rough terrain, whereas bipedal robots are more suited for structured environments such as stairs. Finally, quadruped robots are more stable than bipeds and can carry larger payloads than snakes and bipeds but strugg…
▽ More
The selection of mobility modes for robot navigation consists of various trade-offs. Snake robots are ideal for traversing through constrained environments such as pipes, cluttered and rough terrain, whereas bipedal robots are more suited for structured environments such as stairs. Finally, quadruped robots are more stable than bipeds and can carry larger payloads than snakes and bipeds but struggle to navigate soft soil, sand, ice, and constrained environments. A reconfigurable robot can achieve the best of all worlds. Unfortunately, state-of-the-art reconfigurable robots rely on the rearrangement of modules through complicated mechanisms to dissemble and assemble at different places, increasing the size, weight, and power (SWaP) requirements. We propose Reconfigurable Quadrupedal-Bipedal Snake Robots (ReQuBiS), which can transform between mobility modes without rearranging modules. Hence, requiring just a single modification mechanism. Furthermore, our design allows the robot to split into two agents to perform tasks in parallel for biped and snake mobility. Experimental results demonstrate these mobility capabilities in snake, quadruped, and biped modes and transitions between them.
△ Less
Submitted 2 July, 2021;
originally announced July 2021.
-
Generalizing Non-Punctuality for Timed Temporal Logic with Freeze Quantifiers
Authors:
Shankara Narayanan Krishna,
Khushraj Madnani,
Manuel Mazo Jr.,
Paritosh K. Pandya
Abstract:
Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are prominent real-time extensions of Linear Temporal Logic (LTL). In general, the satisfiability checking problem for these extensions is undecidable when both the future U and the past S modalities are used. In a classical result, the satisfiability checking for MITL[U,S], a non punctual fragment of MTL[U,S], is shown to b…
▽ More
Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are prominent real-time extensions of Linear Temporal Logic (LTL). In general, the satisfiability checking problem for these extensions is undecidable when both the future U and the past S modalities are used. In a classical result, the satisfiability checking for MITL[U,S], a non punctual fragment of MTL[U,S], is shown to be decidable with EXPSPACE complete complexity. Given that this notion of non punctuality does not recover decidability in the case of TPTL[U,S], we propose a generalization of non punctuality called \emph{non adjacency} for TPTL[U,S], and focus on its 1-variable fragment, 1-TPTL[U,S]. While non adjacent 1-TPTL[U,S] appears to be be a very small fragment, it is strictly more expressive than MITL. As our main result, we show that the satisfiability checking problem for non adjacent 1-TPTL[U,S] is decidable with EXPSPACE complete complexity.
△ Less
Submitted 5 September, 2021; v1 submitted 20 May, 2021;
originally announced May 2021.
-
Giant spin-orbit torque efficiency in all-epitaxial heterostructures
Authors:
Nilamani Behera,
Rahul Gupta,
Sajid Husain,
Jitendra Saha,
Rajasekhar Pothala,
Vineet Barwal,
Vireshwar Mishra,
Gabriella Andersson,
Dinesh K. Pandya,
Sujeet Chaudhary,
Rimantas Brucas,
Peter Svedlindh,
Ankit Kumar
Abstract:
A large anti-dam** spin-obit torque (SOT) efficiency in magnetic heterostructures is a prerequisite to realize energy efficient spin torque based magnetic memories and logic devices. The efficiency can be characterized in terms of the spin-orbit fields generated by anti-dam** torques when an electric current is passed through the non-magnetic layer. We report a giant spin-orbit field of 48.96…
▽ More
A large anti-dam** spin-obit torque (SOT) efficiency in magnetic heterostructures is a prerequisite to realize energy efficient spin torque based magnetic memories and logic devices. The efficiency can be characterized in terms of the spin-orbit fields generated by anti-dam** torques when an electric current is passed through the non-magnetic layer. We report a giant spin-orbit field of 48.96 (27.50) mT at an applied current density of 1 MAcm-2 in beta-W interfaced Co60Fe40 (Ni81Fe19)/TiN epitaxial structures due to an anti-dam** like torque, which results in a magnetization auto-oscillation current density as low as 1.68(3.27) MAcm-2. The spin-orbit field value increases with decrease of beta-W layer thickness, which affirms that epitaxial surface states are responsible for the extraordinary large efficiency. SOT induced energy efficient in-plane magnetization switching in large 20x100 um2 structures has been demonstrated by Kerr microscopy and the findings are supported by results from micromagnetic simulations. The observed giant SOT efficiencies in the studied all-epitaxial heterostructures are comparable to values reported for topological insulators. These results confirm that by utilizing epitaxial material combinations an extraordinary large SOT efficiency can be achieved using semiconducting industry compatible 5d heavy metals, which provides immediate solutions for the realization of energy efficient spin-logic devices.
△ Less
Submitted 19 April, 2021;
originally announced April 2021.
-
The Alzheimer's Disease Prediction Of Longitudinal Evolution (TADPOLE) Challenge: Results after 1 Year Follow-up
Authors:
Razvan V. Marinescu,
Neil P. Oxtoby,
Alexandra L. Young,
Esther E. Bron,
Arthur W. Toga,
Michael W. Weiner,
Frederik Barkhof,
Nick C. Fox,
Arman Eshaghi,
Tina Toni,
Marcin Salaterski,
Veronika Lunina,
Manon Ansart,
Stanley Durrleman,
Pascal Lu,
Samuel Iddi,
Dan Li,
Wesley K. Thompson,
Michael C. Donohue,
Aviv Nahon,
Yarden Levy,
Dan Halbersberg,
Mariya Cohen,
Huiling Liao,
Tengfei Li
, et al. (71 additional authors not shown)
Abstract:
We present the findings of "The Alzheimer's Disease Prediction Of Longitudinal Evolution" (TADPOLE) Challenge, which compared the performance of 92 algorithms from 33 international teams at predicting the future trajectory of 219 individuals at risk of Alzheimer's disease. Challenge participants were required to make a prediction, for each month of a 5-year future time period, of three key outcome…
▽ More
We present the findings of "The Alzheimer's Disease Prediction Of Longitudinal Evolution" (TADPOLE) Challenge, which compared the performance of 92 algorithms from 33 international teams at predicting the future trajectory of 219 individuals at risk of Alzheimer's disease. Challenge participants were required to make a prediction, for each month of a 5-year future time period, of three key outcomes: clinical diagnosis, Alzheimer's Disease Assessment Scale Cognitive Subdomain (ADAS-Cog13), and total volume of the ventricles. The methods used by challenge participants included multivariate linear regression, machine learning methods such as support vector machines and deep neural networks, as well as disease progression models. No single submission was best at predicting all three outcomes. For clinical diagnosis and ventricle volume prediction, the best algorithms strongly outperform simple baselines in predictive ability. However, for ADAS-Cog13 no single submitted prediction method was significantly better than random guesswork. Two ensemble methods based on taking the mean and median over all predictions, obtained top scores on almost all tasks. Better than average performance at diagnosis prediction was generally associated with the additional inclusion of features from cerebrospinal fluid (CSF) samples and diffusion tensor imaging (DTI). On the other hand, better performance at ventricle volume prediction was associated with inclusion of summary statistics, such as the slope or maxima/minima of biomarkers. TADPOLE's unique results suggest that current prediction algorithms provide sufficient accuracy to exploit biomarkers related to clinical diagnosis and ventricle volume, for cohort refinement in clinical trials for Alzheimer's disease. However, results call into question the usage of cognitive test scores for patient selection and as a primary endpoint in clinical trials.
△ Less
Submitted 27 December, 2021; v1 submitted 9 February, 2020;
originally announced February 2020.
-
Specification and Optimal Reactive Synthesis of Run-time Enforcement Shields
Authors:
Paritosh K. Pandya,
Amol Wakankar
Abstract:
A system with sporadic errors (SSE) is a controller which produces high quality output but it may occasionally violate a critical requirement REQ(I,O). A run-time enforcement shield is a controller which takes (I,O) (coming from SSE) as its input, and it produces a corrected output O' which guarantees the invariance of requirement REQ(I,O'). Moreover, the output sequence O' must deviate from O "…
▽ More
A system with sporadic errors (SSE) is a controller which produces high quality output but it may occasionally violate a critical requirement REQ(I,O). A run-time enforcement shield is a controller which takes (I,O) (coming from SSE) as its input, and it produces a corrected output O' which guarantees the invariance of requirement REQ(I,O'). Moreover, the output sequence O' must deviate from O "as little as possible" to maintain the quality. In this paper, we give a method for logical specification of shields using formulas of logic Quantified Discrete Duration Calculus (QDDC). The specification consists of a correctness requirement REQ as well as a hard deviation constraint HDC which must both be mandatorily and invariantly satisfied by the shield. Moreover, we also use quantitative optimization to give a shield which minimizes the expected value of cumulative deviation in an H-optimal fashion. We show how tool DCSynth implementing soft requirement guided synthesis can be used for automatic synthesis of shields from a given specification. Next, we give logical formulas specifying several notions of shields including the k-Stabilizing shield of Bloem "et al." as well as the Burst-error shield of Wu "et al.", and a new e,d-shield. Shields can be automatically synthesized for all these specifications using the tool DCSynth. We give experimental results showing the performance of our shield synthesis tool in relation to previous work. We also compare the performance of the shields synthesized under diverse hard deviation constraints in terms of their expected deviation and the worst case burst-deviation latency.
△ Less
Submitted 17 September, 2019;
originally announced September 2019.
-
Specification and Reactive Synthesis of Robust Controllers
Authors:
Paritosh K. Pandya,
Amol Wakankar
Abstract:
This paper investigates the synthesis of robust controllers from logical specification of regular properties given in an interval temporal logic QDDC. Our specification encompasses both hard robustness and soft robustness. Here, hard robustness guarantees invariance of commitment under user-specified relaxed (weakened) assumptions. A systematic framework for logically specifying the assumption wea…
▽ More
This paper investigates the synthesis of robust controllers from logical specification of regular properties given in an interval temporal logic QDDC. Our specification encompasses both hard robustness and soft robustness. Here, hard robustness guarantees invariance of commitment under user-specified relaxed (weakened) assumptions. A systematic framework for logically specifying the assumption weakening by means of a formula, called Robustness Criterion, is presented. The soft robustness pertains to the ability of the controller to maintain the commitment for as many inputs as possible, irrespective of any assumption. We present a uniform method for the synthesis of a robust controller which guarantees the specified hard robustness and it optimizes the specified soft robustness. The method is implemented using a tool DCSynth, which provides soft requirement optimized controller synthesis. Through the case study of a synchronous bus arbiter, we experimentally show the impact of hard robustness criteria as well as soft robustness on the ability of the synthesized controllers to meet the commitment "as much as possible". Both, the worst-case and the expected case behaviors are analyzed.
△ Less
Submitted 27 May, 2019;
originally announced May 2019.
-
DCSYNTH: Guided Reactive Synthesis with Soft Requirements
Authors:
Amol Wakankar,
Paritosh K. Pandya,
Rajmohan Matteplackel
Abstract:
In reactive controller synthesis, a number of implementations (controllers) are possible for a given specification because of the incomplete nature of specification. To choose the most desirable one from the various options, we need to specify additional properties which can guide the synthesis. In this paper, We propose a technique for guided controller synthesis from regular requirements which a…
▽ More
In reactive controller synthesis, a number of implementations (controllers) are possible for a given specification because of the incomplete nature of specification. To choose the most desirable one from the various options, we need to specify additional properties which can guide the synthesis. In this paper, We propose a technique for guided controller synthesis from regular requirements which are specified using an interval temporal logic QDDC. We find that QDDC is well suited for guided synthesis due to its superiority in dealing with both qualitative and quantitative specifications. Our framework allows specification consisting of both hard and soft requirements as QDDC formulas.
We have also developed a method and a tool DCSynth, which computes a controller that invariantly satisfies the hard requirement and it optimally meets the soft requirement. The proposed technique is also useful in dealing with conflicting i.e., unrealizable requirements, by making some of them as soft requirements. Case studies are carried out to demonstrate the effectiveness of the soft requirement guided synthesis in obtaining high-quality controllers. The quality of the synthesized controllers is compared using metrics measuring both the guaranteed and the expected case behaviour of the controlled system. Tool DCSynth facilitates such comparison.
△ Less
Submitted 27 May, 2019; v1 submitted 10 March, 2019;
originally announced March 2019.
-
Extraordinary efficient spin-orbit torque switching in (W, Ta)/epitaxial-Co60Fe40/TiN heterostructures
Authors:
Nilamani Behera,
Rahul Gupta,
Sajid Husain,
Vineet Barwal,
Dinesh K. Pandya,
Sujeet Chaudhary,
Rimantas Brucas,
Peter Svedlindh,
Ankit Kumar
Abstract:
The giant spin Hall effect in magnetic heterostructures along with low spin memory loss and high interfacial spin mixing conductance are prerequisites to realize energy efficient spin torque based logic devices. We report giant spin Hall angle (SHA) of 28.67 (5.09) for W (Ta) interfaced epi- Co60Fe40/TiN structures. The spin-orbit torque switching current density (J_Crit) is as low as 1.82 (8.21)…
▽ More
The giant spin Hall effect in magnetic heterostructures along with low spin memory loss and high interfacial spin mixing conductance are prerequisites to realize energy efficient spin torque based logic devices. We report giant spin Hall angle (SHA) of 28.67 (5.09) for W (Ta) interfaced epi- Co60Fe40/TiN structures. The spin-orbit torque switching current density (J_Crit) is as low as 1.82 (8.21) MA/cm2 in W (Ta)/Co60Fe40(t_CoFe)/TiN structures whose origin lies in the epitaxial interfaces. These structures also exhibit very low spin memory loss and high spin mixing conductance. These extraordinary values of SHA and therefore ultra-low J_Crit in semiconducting industry compatible epitaxial materials combinations open up a new direction for the realization of energy efficient spin logic devices by utilizing epitaxial interfaces.
△ Less
Submitted 2 October, 2019; v1 submitted 8 March, 2019;
originally announced March 2019.
-
Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership
Authors:
Andreas Krebs,
Kamal Lodaya,
Paritosh K. Pandya,
Howard Straubing
Abstract:
We study two extensions of FO2[<], first-order logic interpreted in finite words, in which formulas are restricted to use only two variables. We adjoin to this language two-variable atomic formulas that say, "the letter $a$ appears between positions $x$ and $y$" and "the factor $u$ appears between positions $x$ and $y$". These are, in a sense, the simplest properties that are not expressible using…
▽ More
We study two extensions of FO2[<], first-order logic interpreted in finite words, in which formulas are restricted to use only two variables. We adjoin to this language two-variable atomic formulas that say, "the letter $a$ appears between positions $x$ and $y$" and "the factor $u$ appears between positions $x$ and $y$". These are, in a sense, the simplest properties that are not expressible using only two variables.
We present several logics, both first-order and temporal, that have the same expressive power, and find matching lower and upper bounds for the complexity of satisfiability for each of these formulations. We give effective conditions, in terms of the syntactic monoid of a regular language, for a property to be expressible in these logics. This algebraic analysis allows us to prove, among other things, that our new logics have strictly less expressive power than full first-order logic FO[<]. Our proofs required the development of novel techniques concerning factorizations of words.
△ Less
Submitted 7 September, 2020; v1 submitted 13 February, 2019;
originally announced February 2019.
-
Intent Detection and Slots Prompt in a Closed-Domain Chatbot
Authors:
Amber Nigam,
Prashik Sahare,
Kushagra Pandya
Abstract:
In this paper, we introduce a methodology for predicting intent and slots of a query for a chatbot that answers career-related queries. We take a multi-staged approach where both the processes (intent-classification and slot-tagging) inform each other's decision-making in different stages. The model breaks down the problem into stages, solving one problem at a time and passing on relevant results…
▽ More
In this paper, we introduce a methodology for predicting intent and slots of a query for a chatbot that answers career-related queries. We take a multi-staged approach where both the processes (intent-classification and slot-tagging) inform each other's decision-making in different stages. The model breaks down the problem into stages, solving one problem at a time and passing on relevant results of the current stage to the next, thereby reducing search space for subsequent stages, and eventually making classification and tagging more viable after each stage. We also observe that relaxing rules for a fuzzy entity-matching in slot-tagging after each stage (by maintaining a separate Named Entity Tagger per stage) helps us improve performance, although at a slight cost of false-positives. Our model has achieved state-of-the-art performance with F1-score of 77.63% for intent-classification and 82.24% for slot-tagging on our dataset that we would publicly release along with the paper.
△ Less
Submitted 10 January, 2019; v1 submitted 27 December, 2018;
originally announced December 2018.
-
DCSYNTH: Guided Reactive Synthesis with Soft Requirements for Robust Controller and Shield Synthesis
Authors:
Amol Wakankar,
Paritosh K. Pandya,
Raj Mohan Matteplackel
Abstract:
DCSYNTH is a tool for the synthesis of controllers from safety and bounded liveness requirements given in interval temporal logic QDDC. It investigates the role of soft requirements (with priorities) in obtaining high quality controllers. A QDDC formula specifies past time properties. In DCSYNTH synthesis, hard requirements must be invariantly satisfied whereas soft requirements may be satisfied "…
▽ More
DCSYNTH is a tool for the synthesis of controllers from safety and bounded liveness requirements given in interval temporal logic QDDC. It investigates the role of soft requirements (with priorities) in obtaining high quality controllers. A QDDC formula specifies past time properties. In DCSYNTH synthesis, hard requirements must be invariantly satisfied whereas soft requirements may be satisfied "as much as possible" in a best effort manner by the controller. Soft requirements provide an invaluable ability to guide the controller synthesis. In the paper, using DCSYNTH, we show the application of soft requirements in obtaining robust controllers with various specifiable notions of robustness. We also show the use of soft requirements to specify and synthesize efficient runtime enforcement shields which can correct burst errors. Finally, we discuss the use of soft requirements in improving the latency of controlled system.
△ Less
Submitted 6 November, 2017;
originally announced November 2017.
-
Formalizing Timing Diagram Requirements in Discrete Duration Calulus
Authors:
Raj Mohan Matteplackel,
Paritosh K. Pandya,
Amol Wakankar
Abstract:
Several temporal logics have been proposed to formalise timing diagram requirements over hardware and embedded controllers. These include LTL, discrete time MTL and the recent industry standard PSL. However, succintness and visual structure of a timing diagram are not adequately captured by their formulae. Interval temporal logic QDDC is a highly succint and visual notation for specifying patterns…
▽ More
Several temporal logics have been proposed to formalise timing diagram requirements over hardware and embedded controllers. These include LTL, discrete time MTL and the recent industry standard PSL. However, succintness and visual structure of a timing diagram are not adequately captured by their formulae. Interval temporal logic QDDC is a highly succint and visual notation for specifying patterns of behaviours.
In this paper, we propose a practically useful notation called SeCeCntnl which enhances negation free fragment of QDDC with features of nominals and limited liveness. We show that timing diagrams can be naturally (compositionally) and succintly formalized in SeCeCntnl as compared with PSL and MTL. We give a linear time translation from timing diagrams to SeCeCntnl. As our second main result, we propose a linear time translation of SeCeCntnl into QDDC. This allows QDDC tools such as DCVALID and DCSynth to be used for checking consistency of timing diagram requirements as well as for automatic synthesis of property monitors and controllers. We give examples of a minepump controller and a bus arbiter to illustrate our tools. Giving a theoretical analysis, we show that for the proposed SeCeCntnl, the satisfiability and model checking have elementary complexity as compared to the non-elementary complexity for the full logic QDDC.
△ Less
Submitted 12 May, 2017;
originally announced May 2017.
-
Making Metric Temporal Logic Rational
Authors:
Shankara Narayanan Krishna,
Khushraj Madnani,
P. K. Pandya
Abstract:
We study an extension of $\mtl$ in pointwise time with rational expression guarded modality $\reg_I(\re)$ where $\re$ is a rational expression over subformulae. We study the decidability and expressiveness of this extension ($\mtl$+$\varphi \ureg_{I, \re} \varphi$+$\reg_{I,\re}\varphi$), called $\regmtl$, as well as its fragment $\sfmtl$ where only star-free rational expressions are allowed. Using…
▽ More
We study an extension of $\mtl$ in pointwise time with rational expression guarded modality $\reg_I(\re)$ where $\re$ is a rational expression over subformulae. We study the decidability and expressiveness of this extension ($\mtl$+$\varphi \ureg_{I, \re} \varphi$+$\reg_{I,\re}\varphi$), called $\regmtl$, as well as its fragment $\sfmtl$ where only star-free rational expressions are allowed. Using the technique of temporal projections, we show that $\regmtl$ has decidable satisfiability by giving an equisatisfiable reduction to $\mtl$. We also identify a subclass $\mitl+\ureg$ of $\regmtl$ for which our equi-satisfiable reduction gives rise to formulae of $\mitl$, yielding elementary decidability. As our second main result, we show a tight automaton-logic connection between $\sfmtl$ and partially ordered (or very weak) 1-clock alternating timed automata.
△ Less
Submitted 29 April, 2017;
originally announced May 2017.
-
Deterministic Temporal Logics and Interval Constraints
Authors:
Kamal Lodaya,
Paritosh K. Pandya
Abstract:
In temporal logics, a central question is about the choice of modalities and their relative expressive power, in comparison to the complexity of decision problems such as satisfiability. In this tutorial, we will illustrate the study of such questions over finite word models, first with logics for Unambiguous Starfree Regular Languages (UL), originally defined by Schutzenberger, and then for exten…
▽ More
In temporal logics, a central question is about the choice of modalities and their relative expressive power, in comparison to the complexity of decision problems such as satisfiability. In this tutorial, we will illustrate the study of such questions over finite word models, first with logics for Unambiguous Starfree Regular Languages (UL), originally defined by Schutzenberger, and then for extensions with constraints, which appear in interval logics. We present Deterministic temporal logics, with diverse sets of modalities, which also characterize UL. The tools and techniques used go under the name of "Turtle Programs" or "Rankers". These are simple kinds of automata. We use properties such as Ranker Directionality and Ranker Convexity to show that all these logics have NP satisfiability. A recursive extension of some of these modalities gives us the full power of first-order logic over finite linear orders. We also discuss Interval Constraint modalities extending Deterministic temporal logics, with intermediate expressiveness. These allow counting or simple algebraic operations on paths. The complexity of these extended logics is PSpace, as of full temporal logic (and ExpSpace when using binary notation).
△ Less
Submitted 6 March, 2017;
originally announced March 2017.
-
Machine Learning Approach for Skill Evaluation in Robotic-Assisted Surgery
Authors:
Mahtab J. Fard,
Sattar Ameri,
Ratna B. Chinnam,
Abhilash K. Pandya,
Michael D. Klein,
R. Darin Ellis
Abstract:
Evaluating surgeon skill has predominantly been a subjective task. Development of objective methods for surgical skill assessment are of increased interest. Recently, with technological advances such as robotic-assisted minimally invasive surgery (RMIS), new opportunities for objective and automated assessment frameworks have arisen. In this paper, we applied machine learning methods to automatica…
▽ More
Evaluating surgeon skill has predominantly been a subjective task. Development of objective methods for surgical skill assessment are of increased interest. Recently, with technological advances such as robotic-assisted minimally invasive surgery (RMIS), new opportunities for objective and automated assessment frameworks have arisen. In this paper, we applied machine learning methods to automatically evaluate performance of the surgeon in RMIS. Six important movement features were used in the evaluation including completion time, path length, depth perception, speed, smoothness and curvature. Different classification methods applied to discriminate expert and novice surgeons. We test our method on real surgical data for suturing task and compare the classification result with the ground truth data (obtained by manual labeling). The experimental results show that the proposed framework can classify surgical skill level with relatively high accuracy of 85.7%. This study demonstrates the ability of machine learning methods to automatically classify expert and novice surgeons using movement features for different RMIS tasks. Due to the simplicity and generalizability of the introduced classification method, it is easy to implement in existing trainers.
△ Less
Submitted 15 November, 2016;
originally announced November 2016.
-
Deterministic Logics for UL
Authors:
Paritosh K. Pandya,
Simoni S. Shah
Abstract:
The class of Unambiguous Star-Free Regular Languages (UL) was defined by Schutzenberger as the class of languages defined by Unambiguous Polynomials. UL has been variously characterized (over finite words) by logics such as TL[X_a,Y_a], UITL, TL[F,P], FO2[<], the variety DA of monoids, as well as partially-ordered two-way DFA (po2DFA). We revisit this language class with emphasis on notion of unam…
▽ More
The class of Unambiguous Star-Free Regular Languages (UL) was defined by Schutzenberger as the class of languages defined by Unambiguous Polynomials. UL has been variously characterized (over finite words) by logics such as TL[X_a,Y_a], UITL, TL[F,P], FO2[<], the variety DA of monoids, as well as partially-ordered two-way DFA (po2DFA). We revisit this language class with emphasis on notion of unambiguity and develop on the concept of Deterministic Logics for UL. The formulas of deterministic logics uniquely parse a word in order to evaluate satisfaction. We show that several deterministic logics robustly characterize UL. Moreover, we derive constructive reductions from these logics to the po2DFA automata. These reductions also allow us to show NP-complete satisfaction complexity for the deterministic logics considered.
Logics such as TL[F,P], FO2[<] are not deterministic and have been shown to characterize UL using algebraic methods. However there has been no known constructive reduction from these logics to po2DFA. We use deterministic logics to bridge this gap. The language-equivalent po2DFA for a given TL[F,P] formula is constructed and we analyze its size relative to the size of the TL[F,P] formula. This is an efficient reduction which gives an alternate proof to NP-complete satisfiability complexity of TL[F,P] formulas.
△ Less
Submitted 13 January, 2014;
originally announced January 2014.
-
On the Decidability and Complexity of Some Fragments of Metric Temporal Logic
Authors:
Khushraj Madnani,
Shankara Narayanan Krishna,
Paritosh K. Pandya
Abstract:
Metric Temporal Logic, $\mtlfull$ is amongst the most studied real-time logics. It exhibits considerable diversity in expressiveness and decidability properties based on the permitted set of modalities and the nature of time interval constraints $I$. \oomit{The classical results of Alur and Henzinger showed that $\mtlfull$ is undecidable where as $\mitl$ which uses only non-singular intervals…
▽ More
Metric Temporal Logic, $\mtlfull$ is amongst the most studied real-time logics. It exhibits considerable diversity in expressiveness and decidability properties based on the permitted set of modalities and the nature of time interval constraints $I$. \oomit{The classical results of Alur and Henzinger showed that $\mtlfull$ is undecidable where as $\mitl$ which uses only non-singular intervals $NS$ is decidable. In a surprizing result, Ouaknine and Worrell showed that the satisfiability of $\mtl$ is decidable over finite pointwise models, albeit with NPR decision complexity, whereas it remains undecidable for infinite pointwise models or for continuous time.} In this paper, we sharpen the decidability results by showing that the satisfiability of $\mtlsns$ (where $NS$ denotes non-singular intervals) is also decidable over finite pointwise strictly monotonic time. We give a satisfiability preserving reduction from the logic $\mtlsns$ to decidable logic $\mtl$ of Ouaknine and Worrell using the technique of temporal projections. We also investigate the decidability of unary fragment $\mtlfullunary$ (a question posed by A. Rabinovich) and show that $\mtlfut$ over continuous time as well as $\mtlfullunary$ over finite pointwise time are both undecidable. Moreover, $\mathsf{MTL}^{pw}[\fut_I]$ over finite pointwise models already has NPR lower bound for satisfiability checking. We also compare the expressive powers of some of these fragments using the technique of EF games for $\mathsf{MTL}$.
△ Less
Submitted 27 November, 2013; v1 submitted 27 May, 2013;
originally announced May 2013.
-
The Unary Fragments of Metric Interval Temporal Logic: Bounded versus Lower bound Constraints (Full Version)
Authors:
Paritosh K. Pandya,
Simoni S. Shah
Abstract:
We study two unary fragments of the well-known metric interval temporal logic MITL[U_I,S_I] that was originally proposed by Alur and Henzinger, and we pin down their expressiveness as well as satisfaction complexities. We show that MITL[F_\inf,P_\inf] which has unary modalities with only lower-bound constraints is (surprisingly) expressively complete for Partially Ordered 2-Way Deterministic Timed…
▽ More
We study two unary fragments of the well-known metric interval temporal logic MITL[U_I,S_I] that was originally proposed by Alur and Henzinger, and we pin down their expressiveness as well as satisfaction complexities. We show that MITL[F_\inf,P_\inf] which has unary modalities with only lower-bound constraints is (surprisingly) expressively complete for Partially Ordered 2-Way Deterministic Timed Automata (po2DTA) and the reduction from logic to automaton gives us its NP-complete satisfiability. We also show that the fragment MITL[F_b,P_b] having unary modalities with only bounded intervals has \nexptime-complete satisfiability. But strangely, MITL[F_b,P_b] is strictly less expressive than MITL[F_\inf,P_\inf]. We provide a comprehensive picture of the decidability and expressiveness of various unary fragments of MITL.
△ Less
Submitted 14 May, 2013;
originally announced May 2013.
-
Measurements and ab initio Molecular Dynamics Simulations of the High Temperature Ferroelectric Transition in Hexagonal RMnO3
Authors:
T. A. Tyson,
T. Wu,
H. Y. Chen,
J. Bai,
K. H. Ahn,
K. I. Pandya,
S. B. Kim,
S. -W. Cheong
Abstract:
Measurements of the structure of hexagonal RMnO3 (R=rare earths (Ho) and Y) for temperatures significantly above the ferroelectric transition temperature (TFE) were conducted to determine the nature of the transition. The local and long range structural measurements were complemented by ab initio molecular dynamics simulations. With respect to the Mn sites in YMnO3 and HoMnO3, we find no large ato…
▽ More
Measurements of the structure of hexagonal RMnO3 (R=rare earths (Ho) and Y) for temperatures significantly above the ferroelectric transition temperature (TFE) were conducted to determine the nature of the transition. The local and long range structural measurements were complemented by ab initio molecular dynamics simulations. With respect to the Mn sites in YMnO3 and HoMnO3, we find no large atomic (bond distances or thermal factors), electronic structure changes or rehybridization on crossing TFE from local structural methods. The local symmetry about the Mn sites is preserved. With respect to the local structure about the Ho sites, a reduction of the average Ho-O bond with increased temperature is found. Ab initio molecular dynamics calculations on HoMnO3 reveal the detailed motions of all ions. Above ~900 K there are large displacements of the Ho, O3 and O4 ions along the z-axis which reduce the buckling of the MnO3/O4 planes. The changes result in O3/O4 ions moving to towards central points between pairs of Ho ions on the z-axis. These structural changes make the coordination of Ho sites more symmetric thus extinguishing the electric polarization. At significantly higher temperatures, rotation of the MnO5 polyhedra occurs without a significant change in electric polarization. The born effective charge tensor is found to be highly anisotropic at the O sites but does not change appreciably at high temperatures.
△ Less
Submitted 8 October, 2011;
originally announced October 2011.
-
On Expressive Powers of Timed Logics: Comparing Boundedness, Non-punctuality and Deterministic Freezing
Authors:
Paritosh K. Pandya,
Simoni S. Shah
Abstract:
Timed temporal logics exhibit a bewildering diversity of operators and the resulting decidability and expressiveness properties also vary considerably. We study the expressive power of timed logics TPTL[U,S] and MTL[U,S] as well as of their several fragments. Extending the LTL EF games of Etessami and Wilke, we define MTL Ehrenfeucht-Fraisse games on a pair of timed words. Using the associated EF…
▽ More
Timed temporal logics exhibit a bewildering diversity of operators and the resulting decidability and expressiveness properties also vary considerably. We study the expressive power of timed logics TPTL[U,S] and MTL[U,S] as well as of their several fragments. Extending the LTL EF games of Etessami and Wilke, we define MTL Ehrenfeucht-Fraisse games on a pair of timed words. Using the associated EF theorem, we show that, expressively, the timed logics BoundedMTL[U,S], MTL[F,P] and MITL[U,S] (respectively incorporating the restrictions of boundedness, unary modalities and non-punctuality), are all pairwise incomparable. As our first main result, we show that MTL[U,S] is strictly contained within the freeze logic TPTL[U,S] for both weakly and strictly monotonic timed words, thereby extending the result of Bouyer et al and completing the proof of the original conjecture of Alur and Henziger from 1990. We also relate the expressiveness of a recently proposed deterministic freeze logic TTL[X,Y] (with NP-complete satisfiability) to MTL. As our second main result, we show by an explicit reduction that TTL[X,Y] lies strictly within the unary, non-punctual logic MITL[F,P]. This shows that deterministic freezing with punctuality is expressible in the non-punctual MITL[F,P].
△ Less
Submitted 10 June, 2011; v1 submitted 28 February, 2011;
originally announced February 2011.
