BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Janardan Misra

Janardan Misra contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
Logic in Computer ScienceArtificial IntelligenceComputation and LanguageData Structures and Algorithmsmath.COSoftware Engineering

Trust snapshot

Quick read

Trust 17 - UnverifiedVerification L1Unclaimed author
4works
0followers
6topics
3close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

4 published item(s)

preprint2020arXiv

autoNLP: NLP Feature Recommendations for Text Analytics Applications

While designing machine learning based text analytics applications, often, NLP data scientists manually determine which NLP features to use based upon their knowledge and experience with related problems. This results in increased efforts during feature engineering process and renders automated reuse of features across semantically related applications inherently difficult. In this paper, we argue for standardization in feature specification by outlining structure of a language for specifying NLP features and present an approach for their reuse across applications to increase likelihood of identifying optimal features.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

A Decidable Timeout based Extension of Propositional Linear Temporal Logic

We develop a timeout based extension of propositional linear temporal logic (which we call TLTL) to specify timing properties of timeout based models of real time systems. TLTL formulas explicitly refer to a running global clock together with static timing variables as well as a dynamic variable abstracting the timeout behavior. We extend LTL with the capability to express timeout constraints. From the expressiveness view point, TLTL is not comparable with important known clock based real-time logics including TPTL, XCTL, and MTL, i.e., TLTL can specify certain properties, which cannot be specified in these logics (also vice-versa). We define a corresponding timeout tableau for satisfiability checking of the TLTL formulas. Also a model checking algorithm over timeout Kripke structure is presented. Further we prove that the validity checking for such an extended logic remains PSPACE-complete even in the presence of timeout constraints and infinite state models. Under discrete time semantics, with bounded timeout increments, the model-checking problem that if a TLTL-formula holds in a timeout Kripke structure is also PSPACE complete. We further prove that when TLTL is interpreted over discrete time, it can be embedded in the monadic second order logic with time, and when TLTL is interpreted over dense time without the condition of non-zenoness, the resulting logic becomes $Σ_1^1$-complete.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

A Simplification of a Real-Time Verification Problem

We revisit the problem of real-time verification with dense dynamics using timeout and calendar based models and simplify this to a finite state verification problem. To overcome the complexity of verification of real-time systems with dense dynamics, Dutertre and Sorea, proposed timeout and calender based transition systems to model the behavior of real-time systems and verified safety properties using k-induction in association with bounded model checking. In this work, we introduce a specification formalism for these models in terms of Timeout Transition Diagrams and capture their behavior in terms of semantics of Timed Transition Systems. Further, we discuss a technique, which reduces the problem of verification of qualitative temporal properties on infinite state space of (a large fragment of) these timeout and calender based transition systems into that on clockless finite state models through a two-step process comprising of digitization and canonical finitary reduction. This technique enables us to verify safety invariants for real-time systems using finite state model-checking avoiding the complexity of infinite state (bounded) model checking and scale up models without applying techniques from induction based proof methodology. Moreover, we can verify liveness properties for real-time systems, which is not possible by using induction with infinite state model checkers. We present examples of Fischer's Protocol, Train-Gate Controller, and TTA start-up algorithm to illustrate how such an approach can be efficiently used for verifying safety, liveness, and timeliness properties specified in LTL using finite state model checkers like SAL-smc and Spin. We also demonstrate how advanced modeling concepts like inter-process scheduling, priorities, interrupts, urgent and committed location can be specified as extensions of the proposed specification formalism.

0 citations0 reviewsNo code linkedOpen access
preprint2009arXiv

A Randomized Algorithm for 3-SAT

In this work we propose and analyze a simple randomized algorithm to find a satisfiable assignment for a Boolean formula in conjunctive normal form (CNF) having at most 3 literals in every clause. Given a k-CNF formula phi on n variables, and alpha in{0,1}^n that satisfies phi, a clause of phi is critical if exactly one literal of that clause is satisfied under assignment alpha. Paturi et. al. (Chicago Journal of Theoretical Computer Science 1999) proposed a simple randomized algorithm (PPZ) for k-SAT for which success probability increases with the number of critical clauses (with respect to a fixed satisfiable solution of the input formula). Here, we first describe another simple randomized algorithm DEL which performs better if the number of critical clauses are less (with respect to a fixed satisfiable solution of the input formula). Subsequently, we combine these two simple algorithms such that the success probability of the combined algorithm is maximum of the success probabilities of PPZ and DEL on every input instance. We show that when the average number of clauses per variable that appear as unique true literal in one or more critical clauses in phi is between 1 and 1.9317, combined algorithm performs better than the PPZ algorithm.

0 citations0 reviewsNo code linkedOpen access