0000000000136713

AUTHOR

Parosh Aziz Abdulla

showing 3 related works from this author

General decidability theorems for infinite-state systems

2002

Over the last few years there has been an increasing research effort directed towards the automatic verification of infinite state systems. This paper is concerned with identifying general mathematical structures which can serve as sufficient conditions for achieving decidability. We present decidability results for a class of systems (called well-structured systems), which consist of a finite control part operating on an infinite data domain. The results assume that the data domain is equipped with a well-ordered and well-founded preorder such that the transition relation is "monotonic" (is a simulation) with respect to the preorder. We show that the following properties are decidable for …

Discrete mathematicsRelation (database)ReachabilityData domainPreorderMathematical structurePetri netComputer Science::Formal Languages and Automata TheoryAutomatonDecidabilityMathematics
researchProduct

Algorithmic Analysis of Programs with Well Quasi-ordered Domains

2000

AbstractOver the past few years increasing research effort has been directed towards the automatic verification of infinite-state systems. This paper is concerned with identifying general mathematical structures which can serve as sufficient conditions for achieving decidability. We present decidability results for a class of systems (called well-structured systems) which consist of a finite control part operating on an infinite data domain. The results assume that the data domain is equipped with a preorder which is a well quasi-ordering, such that the transition relation is “monotonic” (a simulation) with respect to the preorder. We show that the following properties are decidable for wel…

Theoretical computer scienceFinite-state machineReachability problemData domainPreorderPetri netComputer Science ApplicationsTheoretical Computer ScienceDecidabilityComputational Theory and MathematicsReachabilityMathematical structureComputer Science::Formal Languages and Automata TheoryInformation SystemsMathematicsInformation and Computation
researchProduct

Simulation is decidable for one-counter nets

1998

We prove that the simulation preorder is decidable for the class of one-counter nets. A one-counter net consists of a finite-state machine operating on a variable (counter) which ranges over the natural numbers. Each transition can increase or decrease the value of the counter. A transition may not be performed if this implies that the value of the counter becomes negative. The class of one-counter nets is computationally equivalent to the class of Petri nets with one unbounded place, and to the class of pushdown automata where the stack alphabet is restricted to one symbol. To our knowledge, this is the first result in the literature which gives a positive answer to the decidability of sim…

Discrete mathematicsClass (set theory)Finite-state machineDeterministic automatonSimulation preorderConcurrencyPushdown automatonPetri netComputer Science::Formal Languages and Automata TheoryDecidabilityMathematics
researchProduct