The primal-dual method for approximation algorithms and its application to network design p

A Stable Primal-Dual Approach for Linear ProgrammingMaria Gonzalez-Lima∗Hua Wei†Henry Wolkowicz‡March10,2007University of WaterlooDepartment of Combinatorics&OptimizationWaterloo,Ontario N2L3G1,CanadaResearch Report CORR2004-26COAP1172-04Key words:Linear Programming,large sparse problems,preconditioned conjugate gradi-ents,stability.AbstractThis paper studies a primal-dual interior/exterior-point path-following approach for linear programming that is motivated on using an iterative solver rather than a direct solver forthe search direction.We begin with the usual perturbed primal-dual optimality equationsFµ(x,y,z)=0.Under nondegeneracy assumptions,this nonlinear system is well-posed,i.e.it has a nonsingular Jacobian at optimality and is not necessarily ill-conditioned asthe iterates approach optimality.We use a simple preprocessing step to eliminate boththe primal and dual feasibility equations.This results in a single bilinear equation thatmaintains the well-posedness property.We then apply both a direct solution techniqueas well as a preconditioned conjugate gradient method(PCG),within an inexact Newtonframework,directly on the linearized equations.This is done without forming the usualnormal equations,NEQ,or augmented system.Sparsity is maintained.The work of aniteration for the PCG approach consists almost entirely in the(approximate)solution of thiswell-posed linearized system.Therefore,improvements depend on efficient preconditioning.。

Helsinki University of Technology Laboratory for Theoretical Computer ScienceResearch Reports76Teknillisen korkeakoulun tietojenka¨sittelyteorian laboratorion tutkimusraportti76Espoo2002HUT-TCS-A76ON MODEL CHECKING SAFETY PROPERTIESTimo LatvalaB TEKNILLINEN KORKEAKOULUTEKNISKA HÖGSKOLANHELSINKI UNIVERSITY OF TECHNOLOGYTECHNISCHE UNIVERSITÄT HELSINKIUNIVERSITE DE TECHNOLOGIE D’HELSINKIHelsinki University of Technology Laboratory for Theoretical Computer Science Research Reports76Teknillisen korkeakoulun tietojenka¨sittelyteorian laboratorion tutkimusraportti76Espoo2002HUT-TCS-A76ON MODEL CHECKING SAFETY PROPERTIESTimo LatvalaHelsinki University of TechnologyDepartment of Computer Science and EngineeringLaboratory for Theoretical Computer ScienceTeknillinen korkeakouluTietotekniikan osastoTietojenka¨sittelyteorian laboratorioDistribution:Helsinki University of Technology Laboratory for Theoretical Computer Science P.O.Box5400FIN-02015HUTTel.+358-0-4511Fax.+358-0-4513369E-mail:lab@tcs.hut.fic Timo LatvalaISBN951-22-6265-7ISSN1457-7615Otamedia OyEspoo2002A BSTRACT:Safety properties are an interesting subset of general temporal properties for systems.In the linear time paradigm,model checking of safety properties is simpler than the general case,because safety properties can be captured byfinite automata.This work discusses the theoretical and some of the practical issues related to model checking LTL properties.Ourfirst contribution is a theorem relating abstraction for Coloured Petri nets as defined by Lakos[36]and preservation of safety properties.We show that a subset of the safety properties are preserved for this abstraction frame-work.Our other contribution is an efficient algorithm for translating LTL safety properties tofinite automata.Minor contributions include new proofs for some old complexity results regarding LTL and safety properties.The implementation of the translation algorithm is also experimentally evaluated.Experiments support the feasibility of the approach.In many tests the implementation is quite competitive when compared to algorithms trans-lating full LTL to Büchi automata.The implementation can also check if an LTL formula is pathologic.The check performs well according to experi-ments.K EYWORDS:Computer aided verification,model checking,LTL,safety properties,abstraction,Coloured Petri netsCONTENTS1Introduction11.1Contributions and Results (2)1.2Related Work (2)1.3Outline (3)2Preliminaries4 3Automata Theoretic Foundations6 4Linear Temporal Logic94.1Syntax and Semantics of LTL (9)4.2Expressiveness and Complexity (11)4.3Safety and Liveness Properties (12)4.4Deciding safety (15)5Abstraction and Safety Properties185.1Coloured Petri Nets (18)5.2Abstraction and Petri Nets (20)5.3Temporal Logic and Refinement (23)5.4An Example (25)6Model Checking Safety Properties286.1Detecting Bad Prefixes (29)6.2Informativeness (31)6.3Translation Algorithm (34)6.4Finite Trace Semantics for LTL (40)7Implementation427.1Translation (42)7.2Checking Pathologic Safety (44)8Translation Experiments468.1Random Formulae (47)Syntactically Safe Formulae (47)General Formulae (49)8.2Model Checking Case Studies (50)9Discussion53 References551INTRODUCTIONDeveloping reliable systems is not an easy task.If the system has concurrencyit is even harder.When concurrency is introduced in a system,phenomenawhich are not present in sequential systems manifest themselves.The in-herent non-determinism of concurrent systems can give rise to subtle errorswhich are very hard to understand and can be difficult to reproduce.Concurrency is a devious source of complexity.Even a simple system can exhibit complex behaviour when concurrency is allowed.This is alsoobvious from many examples in concurrency theory.Determining if afiniteautomaton accepts any string or a given string can be decided with simplelinear-time algorithms.In the concurrent case,i.e.deciding if the intersec-tion of kfinite automata accept any string or a given string,the best knownalgorithms decide the problem in exponential-and linear-time respectively.One of the ways introduced to aid designers in designing correct concur-rent systems is model checking[8,51].Introduced roughly20years ago,model checking has already revolutionised the way hardware systems are de-signed,and can be considered industry practice today[23].The basic idea of model checking is simple.Both the system and the properties the system should have,are expressed as mathematical models.Special algorithms allow comparison of the system against the properties andif the system model violates a property,a violating execution can be displayed.If the model and the properties have been specified correctly,no error will gounnoticed.In the ideal case,all of these stages are automatic and very littlehuman intervention is required.Unsurprisingly,model checking has its limitations.The perhaps most acute problem is how to enable model checking to cope with the ever increas-ing size and complexity of systems.For some classes of systems,the methodsscale quite well.This has made possible the success of model checking inhardware systems.Finding methods which scale for systems which are asyn-chronous and data intensive seems to be more challenging.Consequently,concurrent software systems are still debugged mostly using traditional meth-ods.The problems related to scaling in model checking are referred to as thestate explosion problem[60].In this work we focus on efficient model checking of safety properties,us-ing the automata theoretical approach[62,34,63].Safety properties describeproperties of the system which havefinite counterexamples or,more infor-mally,properties requiring that“nothing bad happens”.A typical safety prop-erty requires e.g.that the value of x always is greater than three.Many com-mon properties such as invariants are safety properties which makes safetyproperties very interesting.In the automata theoretic approach to model checking both the system and the property to be verified are described as automata.The property holdsif all of the executions of the system automaton also are executions of theproperty ually the property is not given as an automaton butin some temporal logic such as linear temporal logic(LTL).There are alsoother logics such as CTL which can be used for specification.In this workwe will mostly restrict ourselves to properties expressed using LTL.This work discusses the theoretical and some of the practical issues of1INTRODUCTION1model checking LTL safety properties.The most relevant complexity resultare presented and analysed.Coloured Petri Nets are one of the formalismsused to describe concurrent systems.We investigate which properties,espe-cially safety properties,are preserved when abstractions defined in[36]areused.Most of this work is dedicated to investigating how to efficiently com-pile an LTL formula into an automaton,when the given formula describes asafety property.Efficient compilation of the formulas facilitates the verifica-tion of larger and more complex systems.1.1Contributions and ResultsWe develop an efficient translation of safety LTL formulae tofinite automata,based on the algorithm presented by Kupferman and Vardi[32].The al-gorithm has been implemented and extensive experiments have been per-formed.Our results show that the algorithm scales better than algorithms fortranslating general LTL formulae to automata.Currently,the implementa-tion is not the fastest of the available translators.However,the experimentsindicate that usingfinite automata for safety model checking results in a realdifference in performance for practical models,especially when the propertydoes not hold.The implementation also includes thefirst implementationto our knowledge of an algorithm for deciding if a formula is a pathologicsafety formula.The work also has some strictly theoretical contributions.Minor contribu-tions include new proofs for some of the complexity results related to safetymodel checking.A more significant contribution is that we show that the ab-straction/refinement framework introduced by Lakos can be used to aid theabstraction when model checking safety properties.We prove that the ab-stractions in the framework preserve a subset of the safety properties in LTL.We also extend the result to some branching time properties.The feasibilityof the approach is argued with a small example.1.2Related WorkModel checking of safety properties has been investigated by number of au-thors.Alpern and Schneider[2]were thefirst to give a formal definitions ofsafety and liveness.The work of Sistla[53]on characterising safety of LTLformulas syntactically continues this work and adds to it significantly.Mostof the automata theoretic insight into safety and liveness comes from Kupfer-man’s and Vardi’s[32]paper.Many important notions are defined there forthefirst time,among them the notions of informativeness for prefixes andclassification of LTL formulae into intentionally,accidentally and patholog-ically safe.The paper also introduces a translation from LTL formulae tofinite automata,which is the basis for the algorithm in this work.Many com-plexity results are also due to them.Geilen[21]also considers translatingLTL intofinite automata.His approach reformulates some of the results ofKupferman and Vardi using their notion of informativeness.The focus ofthe paper is on presenting a tableau algorithm for run-time monitors of LTLproperties.Havelund and Rosu[25]also focus on monitoring executionsof systems.They present a dynamic programming algorithm which checks 21INTRODUCTIONsequences against properties specified in a linear temporal logic with past op-erators.An algorithm for model checking past temporal logic specificationsis also presented in[3].Lakos[36]has defined and introduced most of the concepts related to abstraction and refinement used in this work.He also proved that the refine-ments used are in some sense behaviour respecting.Lewis[41]continuedLakos work and investigated refinement especially in the context of incre-mental development.Lewis also proves that given certain conditions,therefined net is weakly bisimilar to the original net.The approach of Padberget al.[49]is close to the results presented in this paper.They show how arule-based approach for morphisms can be used to stepwise refine nets whilepreserving invariants.1.3OutlineWe begin in Section2by introducing Kripke structures,the system modelused in this work,and by defining some fundamental concepts.Section3gives the automata theoretic foundations,while setting the stage for the au-tomata theoretic approach to model checking employed in this work.Sec-tion4defines LTL and presents the relevant complexity theoretical resultsand clarifies the connection between LTL and automata on infinite words.The important concepts of safety and liveness are also defined and discussedin this section.In Section5abstraction for Coloured Petri Nets w.r.t.modelchecking safety properties is investigated.The translation algorithm fromLTL tofinite automata is given in Section5.Section6discusses imple-mentation issues while Section7focuses on experimentally evaluating theperformance of the algorithm.Section8discusses the results and speculateson possible future work.1INTRODUCTION32PRELIMINARIESFormal languages.A very important concept in this work is the concept oflanguages.LetΣbe afinite set called the alphabet.Afinite word of lengthn overΣis a mapping w:{1,2,...,n}→Σ.Words are also in many casespresented as strings w=σ0σ1...σn,whereσi∈Σ.A language offinitewords overΣis a set L offinite words.We can also talk about infinite words.They are mappings w:N→Σ.Languages are defined as in thefinite wordcase.Regular expressions.One way we will define languages in this work is using regular expressions.We define the syntax of regular expressions w.r.t.an alphabet.•Every letter from the alphabet is a regular expression.•Ifαandβare regular expressions,then so are ,(α∪β),(αβ)andα∗Every regular expression defines a language.The letterσ∈Σdefines theone-word language{σ}.By we denote the empty string and(α∪β)is theunion of the languages ofαandβ.With(αβ)we denote the concatenationof the languages ofαandβ.In some cases the shorthandαi=αα···α,i.e.αi times,is used.The Kleene star,α∗is defined through the union:α∗= ∪ i∈N+αiIn many cases our alphabet will be2Σ.In this case we will use booleanterms overΣto define sets of letters.IfΣ={a,b},then a∨b denotes{{a},{b},{a,b}}while¬a denotes{∅,{b}}.The expression can be seenas a shorthand for2Σ.Formal models.All formal reasoning requires a formal model of the sys-tem under inspection.In this work we will consider the common modelwhere time is discrete and no concept of duration exists.This means thatthe ordering between events is relevant,but time between events is not.Ateach point in time,the system can be described by its state.The behaviour ofthe system is the possible sequences of states of the system.All behaviours ofthe system are considered infinite.For the class of systems we are especiallyfocusing on,reactive systems,this assumption is easy to justify.Reactive sys-tems continuously react to inputs from the environment and they have nonatural terminating state.Abstractly,their behaviour can be seen as infinite.It is of course possible that the system,e.g.due to a programming error,en-ters a state from which it cannot proceed.This can,however,be simulatedby having the system loop in the same state.The notions above can be formalised using the Kripke structure model.The model is very simple and abstract,but it will be sufficient for our pur-poses most of the ter we will also introduce higher-level formalismswhich are closer to programming languages.These mainly function as gen-erators of Kripke structures.Definition1A Kripke structure is a tuple M= S,δ,s0,π ,where•S is a set of states,42PRELIMINARIES•δ⊆S×S is the transition relation obeying the condition that∀s∈S:∃s ∈S:(s,s )∈δ,•s0is the initial state of the system,and•π:S→2AP is a labelling function which assigns a set of atomicpropositions to each state.An execution of a Kripke structure M is an infinite sequence of statesσ=s0s1s2...,where s0is the initial state of M and(s i,s i+1)∈δ.The set of states S can be eitherfinite or infinite.Most definitions in thiswork are oblivious to this,however,a few of the algorithms requirefinitenessfor termination.We can also define the language of a Kripke structure.An executionσcan be projected onto the alphabet2AP by using the labelling functionπ.This projected sequence can be considered a word in(2AP)ω.The set of exe-cutions of the Kripke structure generates a set of infinite words,the languageof the Kripke structure,denoted L(M).The relation between executions and infinite words will allow us to use automata theory to specify behaviours of systems.This is one of the fun-damental ideas which underlies the automata theoretic approach to modelchecking.2PRELIMINARIES53AUTOMATA THEORETIC FOUNDATIONSFinite automata onfinite an infinite words are essential constructs for the au-tomata theoretic approach to verification.This section introduces alternatingautomata and non-deterministic automata.Just asfinite automata onfinite words are equivalent to regular languages finite automata on infinite words are equivalent to omega-regular langua-ges(c.f.[59]).Omega-regular languages are like the normal regular lan-guages but an additional operator,ω,is allowed for omega-regular expres-sions.The expression(a∪b)(ba)ωcharacterises all strings which start witha orb and are followed by infinitely many ba:s.In the following we considerwords defined over an alphabetΣ.Let X be afinite set and B+(X)the set of all positive Boolean formulas over X including the abbreviations true and false.A set Y⊆X satisfies aformulaθ∈B+(X)iffθis satisfied by setting all the elements in Y to trueand all elements in X\Y to false.For the familiar non-deterministic automaton,if Q is a set of states,a tran-sition relationδcan be defined asδ⊆Q×Σ×Q.A transitionδ(q,σ)={q1,q2,q3}maps a state and a letterσ∈Σto a set of states.The non-deterministic nature of the automaton allows it to move to several states inone transition.Alternating automata generalise this by allowing the automa-ton use a bounded number of copies of itself which work non-determinis-tically.Formally,transitions are mapped to arbitrary positive formulas inB+(Q).As an example,if we have the transitionδ(q,σ)=q1∧(q2∨q3),theautomaton moves to the states q1and non-deterministically to q2or q3.Letw=σ0σ1...be a word and let w i=σiσi+1...denote the suffix of w startingfrom the i:th position.The automaton above accepts a suffix w l from q if itaccepts w l+1both from q1and from either q2or q3.In this framework thenon-deterministic transition above is expressed asδ(q,σ)=q1∨q2∨q3Non-deterministic automata are thus automata where only the or-connective is al-lowed in the transition relation.Non-determinism captures existential choicewith the perfect guessing capability of the automata.Non-determinism caneasily capture existential style questions such as“accept any word which hasthe property p”.Alternating automata can succinctly express both universaland existential choice.When a word w=σ0σ1...is read by an automaton it induces runs of the automaton.For a non-deterministic automaton a run can be seen as afunction r:N→Q,where r(0)is an initial state and for every i≥0,r(i+1)is inδ(r(i),σi).Each position is mapped to a state of the automatonand the run must respect the transition relation of the automaton.Due tonon-determinism,one word induces several runs.Runs for an alternating automaton are not so simple.An alternating au-tomaton can be seen as making copies of it self,when“and”appears in atransition.A run of an alternating automaton is thus better viewed as a la-belled tree rather than as a path as for non-deterministic automata.A tree isa non-empty set T⊆N∗,where for every x·c∈T with x∈N∗and c∈N wehave x∈T.The elements of T are called nodes and the empty word is theroot of T.For x·c∈T,x∈T is the unique parent of x·c,and respectivelyall x·c∈T are the children x.A node without children is called a leaf.The 63AUTOMATA THEORETIC FOUNDATIONSlevel of a node is its distance from the root .A pathπ=x0x1...of a treeis a maximal sequence of nodes such that x0is the root and x i is the parentof x i+1for all i≥0.AΣ-labelled tree is a pair T,V ,where T is a tree andV:T→Σmaps each node of T to a letter inΣ.Definition2An alternating automaton is tuple A= Σ,Q,δ,Q0,F where•Σis the input alphabet,•Q is afinite set of states,•δ:Q×Σ→B+(Q)is a transition function,•Q0⊆Q is a set of initial states and,•F⊆Q is a set offinal states.A run of A over an infinite word w=σ0σ1...is a Q-labelled tree T r,r ,where T⊆N∗and r( )∈Q0.For every node x∈T r withδ(r(x),σ|x|+1)=θthere is a possibly empty set{r(x·c)|x·c∈T r}which satisfiesθ.Withthe Büchi accepting condition,A accepts a run T r,r if all infinite pathsπ⊆T r visit at least one state in F infinitely often.A word is accepted if thereexists an accepting run for it.Ifδ(r(x),σi)=true,then x does not need to have any children.Thus allbranches of the tree need not be infinite in the run.On the other hand falsemust not appear in a run,since false is not satisfiable.The special cases of non-deterministic and deterministic are easy to de-fine.An automaton A is non-deterministic iffδ(q,σ)uses only disjunctions.A is deterministic iffδ(q,σ)∈(Q∪false)and|Q0|=1.The Büchi ac-cepting condition is the obvious:a run r:N→Q is accepted if at least onestate in F is visited infinitely often in the run and a word is accepted if hasan accepting run.Alternating automata can also acceptfinite words.A run on afinite word w=σ0σ1...σn is afinite Q-labelled tree T r,r with T⊆N≤n,where N≤nis set of N-words not longer than n.Otherwise,a run is defined in the sameway as in the infinite word case.A run is accepted iff for all nodes x of leveln we have that r(x)∈F.The set of words an automaton A accepts is denoted L(A)and is called the language of A.If L(A)=∅the automaton is called empty.Alternation does not increase the expressive power offinite automata.Al-ternating automata onfinite words define a regular language and alternatingautomata on infinite words an omega-regular language(c.f.[63]).However,both in thefinite and the infinite word case,alternating automata can beexponentially more succinct than non-deterministic automata.The transla-tion of an alternating automaton to afinite automaton constructs an non-deterministic automaton which is exponentially larger.In the general case,the blow-up is unavoidable.The intuitive idea behind the translation is thatthefinite automaton guesses a run tree of the alternating automaton.At agiven point of a run,thefinite automaton keeps a whole level in memory.When it reads the next symbol it guesses the next level.3AUTOMATA THEORETIC FOUNDATIONS7Allfinite automata are closed under union,intersection and complemen-tation.While complementing non-deterministic automata involves an ex-ponential penalty,alternating automata on infinite words can be comple-mented with only a quadratic blow up[31]and alternating automata onfinitewords complemented in linear time(c.f.[63]).In many applications it is important to determine if the automaton is empty.For a non-deterministic automaton onfinite words,determining ifthe automaton is empty can be done in linear time simply by checking if anyfinal state is reachable from an initial state using the normal graph traversalalgorithms.The problem can be shown to be NLOGSPACE-complete usingthe reachability method(c.f.[63]).An automaton on infinite words is non-empty if there exists a path from an initial state to afinal state,and thefinal state can be reached from itself.Despite the algorithmically more challenging task,the linear time bound canbe maintained in the following way.The strongly connected components(SCC)of the automaton can be computed in linear time[56].If a non-trivial SCC contains afinal state the automaton is ing thereachability method this problem can also be shown to be NLOGSPACE-complete.Unsurprisingly emptiness checking for alternating automata is much more challenging.For both thefinite word and infinite word case,it is in factPSPACE-complete.Proposition3([6])The non-emptiness problem for alternating automata isPSPACE-completeProof:An alternating automaton can be translated into a non-deterministic automa-ton with an exponential blow-up[6].Non-deterministic automata can betested for emptiness in logarithmic space and thus if we do the translationand the emptiness checking on-the-fly,we get a polynomial space algorithm.To prove PSPACE-hardness of the emptiness problem we can reduce, as we later shall see,the validity problem for LTL to the emptiness prob-lem(c.f.[63]). 83AUTOMATA THEORETIC FOUNDATIONS4LINEAR TEMPORAL LOGICTemporal logic[50]is a popular way of specifying properties of reactive sys-tems.There are two basic variants of temporal logic,linear and branch-ing[37].In linear temporal logic(LTL),introduced to the verification settingby Pnueli[50],any given point in time has only one future,while branch-ing time logics[37]allows several possible futures.The perhaps most knownbranching time logic is computation tree logic(CTL),introduced in[15].There has been a two decade long debate,albeit currently not so in-tense,among researchers in the concurrency community which paradigm,the branching or the linear,is superior in reasoning about concurrency.Tothe author’s knowledge,the most recent contribution to this debate is[64].In this work,we almost exclusively focus on the linear paradigm.The primary reason is that current research indicates[32]that the concept ofsafety does not seem to be as fruitful in the branching time paradigm.LTL allows properties of systems be specified easily,especially compared to e.g.first order logic.The great innovation of Pnueli[50]was that thismodal logic was suitable for this mon properties like invariants,fairness and causal relationships can be concisely expressed without the hor-de of quantifiers thatfirst order logic would require.LTL also enjoys a complexity advantage compared to fullfirst order logic.It is expressive enough in most cases.In contrast,solving thefirst order logicmodel checking problem is non-elementary(c.f.[9]).4.1Syntax and Semantics of L TLThe syntax of LTL consists of atomic propositions,the normal boolean con-nectives,and temporal operators.Let AP be a set of atomic propositions.Well-formed formulae of LTL are constructed in the following way:•true,false and every p∈AP are well-formed formulae•Ifψandϕare well-formed formulae,then so areψ∧ϕ,ψ∨ϕ,ψUϕ,ψVϕ,¬ϕand Xϕ.LTL is interpreted over infinite sequences of atomic propositions,i.e.infinitewords in(2AP)ω.A model(or word)π=σ0σ1σ2...,whereσi⊆AP,is amappingπ:N→2AP.Byπi we denote the suffixπi=σiσi+1σi+2...andπi denotes the prefixπi=σ0σ1...σi.For an LTL formulaψand a modelπ,we writeπi|=ψ,“the suffixπi is a model ofψ”.The semantics of themodels relation|=is defined inductively in the following way.•For allπi we have thatπi|=true andπi|=false.•For atomic propositions p∈AP,πi|=p iff p∈σi•πi|=ψ1∨ψ2iffπi|=ψ1orπi|=ψ2.•πi|=ψ1∧ψ2iffπi|=ψ1andπi|=ψ2.•πi|=Xψiffπi+1|=ψ.•πi|=¬ψiffπi|=ψ.4LINEAR TEMPORAL LOGIC9•πi|=ψ1Uψ2iff there exists k≥i such thatπk|=ψ2and for alli≤j<kπj|=ψ1.•πi|=ψ1Vψ2iff for all k≥i,ifπk|=ψ2,then there is i≤j<k suchthatπj|=ψ1.Usually we do not writeπ0|=ψbut simplyπ|=ψ.Other commonlyused abbreviations are Fψ=true Uψ,Gψ=false Vψ,and the normalabbreviations for the boolean connectives⇒,⇔.Of interest is also the un-less-operator W which is defined by the equivalenceψ1Wψ2≡ψ1Uψ2∨Gψ1.A sufficient set of operators which can express all LTL-properties is∨,U,X,¬.Note also the duality between until and release,¬(ψ1Uψ1)≡¬ψ1V¬ψ2.The operator X is the so called next-operator which requires that a formula is true in the next position of the execution.The binary operator U is calledthe until-operator.ψ1Uψ2means that eventuallyψ2will be true,and untilthenψ1is true.This version of the until-operator is called reflexive becausethe operator is satisfied ifψ2is true immediately.The dual of until,V,iscalled the release-operator.The formulaψ1Vψ2requires thatψ2is true ifψ1has not been true at an earlier point of time.In this caseψ1andψ2must besimultaneously true at some point.Note thatψ1is not required to eventuallybecome true.The operator G has the meaning“globally”or“henceforth”.It requires that a formula is true in all positions from the current onward.The dual of G is F,called“finally”or“eventually”.The meaning of Fψisthatψmust be true at the current point or at some point in the future.Theunless-operator,W,also known as the weak until operator,says that thefirstargument holds at least up until the second argument.The second argumentis never required to hold though.An LTL formulaψspecifies a language L(ψ)={π∈(2AP)ω|π|=ψ}.The connection between the executions of a Kripke structure and the mod-els of an LTL formula is now clear.The executions generate words over2AP,which can also be interpreted as models of an LTL formula.Thus,given aKripke structure M and an LTL formulaψ,we write M|=ψiff the pro-jection to the atomic propositions of the LTL formula of each execution ofthe Kripke structure M is a model ofψ.Sometimes this is referred to as theuniversal model checking problem.The dual of the universal model check-ing problem is the existential model checking problem where we ask if anyexecution of the Kripke structure satisfies the given formula.Example4Writing simple properties in LTL is fairly straightforward.Speci-fying an invariant is easy.Let p be the atomic proposition having the meaningthat the variable x is greater than zero.Claiming that this is an invariant iseasy:G pRequiring that x will always return to state where it is greater than zero is notmuch more difficult:GF pCausal relationships are also easily expressed.If p is an atomic propositionmeaning that“A goes up”and q means“A comes down”formalising“if A 104LINEAR TEMPORAL LOGIC。

Fast,Approximately Optimal Solutions for Single and Dynamic MRFs∗Nikos Komodakis,Georgios Tziritas University of Crete,Computer Science Department {komod,tziritas}@csd.uoc.grNikos Paragios MAS,Ecole Centrale de Paris nikos.paragios@ecp.frAbstractA new efficient MRF optimization algorithm,called Fast-PD,is proposed,which generalizesα-expansion.One ofits main advantages is that it offers a substantial speedupover that method,e.g.it can be at least3-9times fasterthanα-expansion.Its efficiency is a result of the fact thatFast-PD exploits information coming not only from the orig-inal MRF problem,but also from a dual problem.Further-more,besides static MRFs,it can also be used for boost-ing the performance of dynamic MRFs,i.e.MRFs varyingover time.On top of that,Fast-PD makes no compromiseabout the optimality of its solutions:it can compute exactlythe same answer asα-expansion,but,unlike that method,itcan also guarantee an almost optimal solution for a muchwider class of NP-hard MRF problems.Results on staticand dynamic MRFs demonstrate the algorithm’s efficiencyand power.E.g.,Fast-PD has been able to compute dispar-ity for stereoscopic sequences in real time,with the resultingdisparity coinciding with that ofα-expansion.1.IntroductionDiscrete MRFs are ubiquitous in computer vision,andthus optimizing them is a problem of fundamental impor-tance.According to it,given a weighted graph G(withnodes V,edges E and weights w pq),one seeks to assigna label x p(from a discrete set of labels L)to each p∈V,sothat the following cost is minimized:p∈Vc p(x p)+ (p,q)∈E w pq d(x p,x q).(1)Here,c p(·),d(·,·)determine the singleton and pairwiseMRF potential functions respectively.Up to now,graph-cut based methods,likeα-expansion[3],have been very effective in MRF optimization,generat-ing solutions with good optimality properties[8].However,besides solutions’optimality,another important issue is thatof computational efficiency.In fact,this issue has recentlybeen looked at for the special case of dynamic MRFs[5,4],i.e.MRFs varying over time.Thus,trying to concentrate onboth of these issues here,we raise the following questions:can there be a graph-cut based method,which will bemore efficient,but equally(or even more)powerful,thanα-expansion,for the case of single MRFs?Furthermore,1Fast-PD requires only d(a,b)≥0,d(a,b)=0⇔a=b1:[x,y]←INIT PRIMALS();x old←x 2:for each label c in L do3:y←PREEDITDUALSDUALS(c,x′,y′);6:x←x′;y←y′; 7:end for8:if x=x old then 9:x old←x;goto2; 10:end ifFig.1:The primal dual schema for MRF optimization. single MRFs is further analyzed in sec.4,where related results and some important extensions of Fast-PD are presented as well.Sec.5explains how Fast-PD can boost the performance of dynamic MRFs,and also contains more experimental results.Finally,we conclude in section6. 2.Primal-dual MRF optimization algorithmsIn this section,we review very briefly the work of[6]. Consider the primal-dual pair of linear programs,given by: P RIMAL:min c T x D UAL:max b T ys.t.Ax=b,x≥0s.t.A T y≤c One seeks an optimal primal solution,with the extra con-straint of x being integral.This makes for an NP-hard prob-lem,and so one can only hope forfinding an approximate solution.To this end,the following schema can be used: Theorem1(Primal-Dual schema).Keep generating pairs of integral-primal,dual solutions(x k,y k),until the ele-ments of the last pair,say x,y,are both feasible and have costs that are close enough,e.g.their ratio is≤f app:c T x≤f app·b T y(2) Then x is guaranteed to be anf app-approximate solution to the optimal integral solution x∗,i.e.c T x≤f app·c T x∗.The above schema has been used in[6],for deriving ap-proximation algorithms for a very wide class of MRFs.To this end,MRF optimization wasfirst cast as an equivalent integer program and then,as required by the primal-dual schema,its linear programming relaxation and its dual were derived.Based on these LPs,the authors then show that,for Theorem1to be true with f app=2d max2d max≡max a=b d(a,b),d min≡min a=b d(a,b)h p(·)≡c p(·)+ q:qp∈E y pq(·).(6) Note that,due to(6),only the vector y(of all balance vari-ables)is needed for specifying a dual solution.In addition, for simplifying conditions(4),(5),one can also define:load pq(a,b)≡y pq(a)+y qp(b).(7) The primal-dual variables are iteratively updated until all conditions(3)-(5)hold true.The basic structure of a primal-dual algorithm can be seen in Fig.1.During an inner c-iteration(lines3-6in Fig.1),a label c is selected and a new primal-dual pair of solutions(x′,y′)is generated based on the current pair(x,y).To this end,among all bal-ance variables y pq(.),only the balance variables of c-labels (i.e.y pq(c))are updated during a c-iteration.|L|such itera-tions(i.e.one c-iteration per label c in L)make up an outer iteration(lines2-7in Fig.1),and the algorithm terminates if no change of label takes place at the current outer iteration.During an inner iteration,the main update of the primal and dual variables takes place inside UP-DATE PRIMALS,and(as shown in[6])this update reduces to solving a max-flow problem in an appropriate graph G c.Furthermore,the routines PREEDITDUALS simply apply corrections to the dual variables before and after this main update,i.e.to variables y and y′respectively.Also,for simplicity’s sake,note that we will hereafter refer to only one of the methods derived in[6],and this will be the so-called PD3a method.3.Fast primal-dual MRF optimizationThe complexity of the PD3a primal-dual method largely depends on the complexity of all max-flow instances(one instance per inner-iteration),which,in turn,depends on the number of augmentations per max-flow.So,for designing faster primal-dual algorithms,wefirst need to understand how the graph G c,associated with the max-flow problem at a c-iteration of PD3a,is constructed.To this end,we also have to recall the following intuitive interpretation of the dual variables[6]:for each node p,a separate copy of all la-bels in L is considered,and all these labels are represented as balls,whichfloat at certain heights relative to a reference plane.The role of the height variables h p(·)is then to deter-mine the balls’height(see Figure2(a)).E.g.the height of label a at node p is given by h p(a).Also,expressions like “label a at p is below/above label b”imply h p(a)≶h p(b). Furthermore,balls are not static,but may move in pairs through updating pairs of conjugate balance variables.E.g., in Figure2(a),label c at p is raised by+δ(due to adding+δto y pq(c)),and so label c at q has to move down by−δ(due to adding−δto y qp(c)so that condition y pq(c)=−y qp(c) still holds).Therefore,the role of balance variables is to raise or lower labels.In particular,the value of balance vari-able y pq(a)represents the partial raise of label a at p due to edge pq,while(by(6))the total raise of a at p equals the sum of partial raises from all edges of G incident to p.nodes{p,q}and2labels{a,c}.A copy of labels{a,c}exists for every node,and all these labels are represented by ballsfloating at certain heights.The role of the height variables h p(·)is to specify exactly these heights.Furthermore,balls are not static,but may move(i.e.change their heights)in pairs by updating conjugate balance variables.E.g.,here,ball c at p is pulled up by+δ(due to increasing y pq(c)by+δ)and so ball c at q moves down by −δ(due to decreasing y qp(c)by−δ).Active labels are drawn with a thicker circle.(b)If label c at p is below x p,then(due to(3))we want label c to raise and reach x p.We thus connect node p to the source s with an edge s p(i.e.p is an s-linked node),andflow f s p represents the total raise of c(we also set cap s p=h p(x p)−h p(c)).(c)If label c at p is above x p,then (due to(3))we want label c not to go below x p.We thus connect node p to the sink t with edge p t(i.e.p is a t-linked node),and flow f p t represents the total decrease in the height of c(we also set cap p t=h p(c)−h p(x p)so that c will still remain above x p).Hence,PD3a tries to iteratively move labels up or down, until all conditions(3)-(5)hold true.To this end,it uses the following strategy:it ensures that conditions(4)-(5)hold at each iteration(which is always easy to do)and is just left with the main task of making the labels’heights satisfy con-dition(3)as well in the end(which is the most difficult part, requiring each active label x p to be the lowest label for p). For this purpose,labels are moved in groups.In particular, during a c-iteration,only the c-labels are allowed to move. Furthermore,it was shown in[6]that the movement of all c-labels(i.e.the update of dual variables y pq(c)and h p(c) for all p,q)can be simulated by pushing the maximumflow through a directed graph G c(which is constructed based on the current primal-dual pair(x,y)at a c-iteration).The nodes of G c consist of all nodes of graph G(the internal nodes),plus2external nodes,the source s and the sink t. In addition,all nodes of G c are connected by two types of edges:interior and exterior edges.Interior edges come in pairs pq,qp(with one such pair for every2neighbors p,q in G),and are responsible for updating the balance variables. In particular,theflows f pq/f qp of these edges represent the increase/decrease of balance variable y pq(c),i.e.y′pq(c)= y pq(c)+f pq−f qp.Also,as we shall see,the capacities of interior edges are used together with PREEDITDUALS to impose conditions(4),(5).But for now,in order to understand how to make a faster primal-dual method,it is the exterior edges(which are in charge of the update of height variables),as well as their capacities(which are used for imposing the remaining condition(3)),that are of interest to us.The reason isthat these edges determine the number of s-linked nodes, which,in turn,affects the number of augmenting pathsper max-flow.In particular,each internal node connects toeither the source s(i.e.it is an s-linked node)or to the sink t(i.e.it is a t-linked node)through one of these exterior edges,and this is done(with the goal of ensuring(3))as follows:if label c at p is above x p during a c-iteration(i.e.h p(c)>h p(x p)),then label c should not go below x p,or else(3)will be violated for p.Node p thus connects to t through directed edge p t(i.e.p becomes t-linked),andflowf p t represents the total decrease in the height of c after UPDATE PRIMALS,i.e.h′p(c)=h p(c)−f p t(see Fig. 2(c)).Furthermore,the capacity of p t is set so that label cwill still remain above x p,i.e.cap p t=h p(c)−h p(x p).On the other hand,if label c at p is below active label x p(i.e.h p(c)<h p(x p)),then(due to(3))label c should raise so as to reach x p,and so p connects to s through edge s p(i.e. p becomes s-linked),whileflow f s p represents the total raise of ball c,i.e.h′p(c)=h p(c)+f s p(see Fig.2(b)).In this case,we also set cap s p=h p(x p)−h p(c).This way,by pushingflow through the exterior edgesof G c,all c-labels that are strictly below an active label try to raise and reach that label during UPDATE PRIMALS3.Not only that,but the fewer are the c-labels below an active label(i.e.the fewer are the s-linked nodes), the fewer will be the edges connected to the source,and thus the less will be the number of possible augmenting paths. In fact,the algorithm terminates when,for any label c,there are no more c-labels strictly below an active label(i.e.no s-linked nodes exist and thus no augmenting paths may be found),in which case condition(3)willfinally hold true, as desired.Put another way,UPDATE PRIMALS tries to push c-labels(which are at a low height)up,so that the number of s-linked nodes is reduced and thus fewer augmenting paths may be possible for the next iteration.However,although UPDATE PRIMALS tries toreduce the number of s-linked nodes(by pushing the maxi-mum amount offlow),PREEDIT DU-ALS very often spoil that progress.As we shall see later, this occurs because,in order to restore condition(4)(which is their main goal),these routines are forced to apply correc-tions to the dual variables(i.e.to the labels’height).This is abstractly illustrated in Figure3,where,as a result of push-ingflow,a c-label initially managed to reach an active label x p,but it again dropped below x p,due to some correction applied by these routines.In fact,as one can show,the only point where a new s-linked node can be created is during either PREEDIT DUALS.DUALSDUALSh)h(c)PREEDIT_DUALS or POSTEDIT_DUALS Fig.3:(a)Label c at p is below x p,and thus label c is allowed to raise itself in order to reach x p.This means that p willbe an s-linked node of graph G c,i.e.caps p>0,and thus a non-zeroflow f s p(representing the total raise of label c)may pass through edge s p.Therefore,in this case,edge s p may become part of an augmenting path during max-flow.(b)After UPDATE PRIMALS,label c has managed to raise by f s p and reach x p.Since it cannot go higher than that,noflow can passthrough edge s p,i.e.caps p=0,and so no augmenting path may traverse that edge thereafter.(c)However,due to some correction applied to c-label’s height,label c has dropped below x p oncemore and p has become an s-linked node again(i.e.caps p>0). Edge s p can thus be part of an augmenting path again(as in(a)).Tofix this problem,we will redefine PREEDITDUALS so that they can now ensure condition(4) by using just a minimum amount of corrections for the dual variables,(e.g.by touching these variables only rarely).To this end,however,UPDATE PRIMALS needs to be modified as well.The resulting algorithm,called Fast-PD, carries the following main differences over PD3a during a c-iteration(its pseudocode appears in Fig.4):-the new PREEDITDUALSDUALS can be shown to be the minimal correction that restores exactly the above inequ-alities(assuming,of course,this restoration is possible).-Similarly,the new POSTEDITDUALS simply has toDUALS may modify only dual solution y′. For that solution,we define load′pq(a,b)≡y′pq(a)+y′qp(b),as in(7).[x,y]←INIT PRIMALS():x←random labels;y←0;∀pq,adjust y pq(x p)or y qp(x q)so that load pq(x p,x q)=w pq d(x p,x q) y←PREEDITDUALSDUALS(c,x′,y′):{We denote load′pq(·,·)=y′pq(·)+y′qp(·)}∀pq,if load′pq(x′p,x′q)>w pq d(x′p,x′q){This implies x′p=c or x′q=c} adjust y′pq(c)so that load′pq(x′p,x′q)=w pq d(x′p,x′q)Fig.4:Fast-PD’s pseudocode.reduce load′pq(x′p,x′q)for restoring(4).However,this inequality will hold true very rarely(e.g.for a metric d(·,·), one may show that it can never hold),and so POSTEDITDU-ALSDUALS for all but a few p,q).For seeing this, the crucial thing to observe is that if,say,(c,x q)are the next labels for p and q,then capacity cap pq can be shown to represent the increase of load pq(c,x q)after max-flow,i.e.: load′pq(c,x q)=load pq(c,x q)+cap pq.(10) Hence,if the following inequality is true as well:load pq(c,x q)≤w pq d(c,x q),(11) then condition(4)will do remain valid after max-flow,as the following trivial derivation shows:load′pq(c,x q)(10),(8)=load pq(c,x q)+[w pq d(c,x q)−load pq(c,x q)]+(11)=w pq d(c,x q)(12) But this means that a correction may need to be applied by POSTEDITDUALS,POSTEDIT5If c=x p or c=x q,then cappq=cap qp=0as before,i.e.as in PD3a.in a few cases)allow UPDATE PRIMALS to impose conditions(4),(5),while the exterior capacities allow UP-DATE PRIMALS to impose condition(3).As a re-sult,the next theorem holds(see[1]for a complete proof):Theorem2.The last primal-dual pair(x,y)of Fast-PD satisfies(3)-(5),and so x is an f app-approximate solution.In fact,Fast-PD maintains all good optimality proper-ties of the PD3a method.E.g.,for a metric d(·,·),Fast-PD proves to be as powerful asα-expansion(see[1]): Theorem3.If d(·,·)is a metric,then the Fast-PD algo-rithm computes the best c-expansion after any c-iteration.4.Efficiency of Fast-PD for single MRFsBut,besides having all these good optimality properties, a very important advantage of Fast-PD over all previous primal-dual methods,as well asα-expansion,is that it proves to be much more efficient in practice.In fact,the computational efficiency for all methods of this kind is largely determined from the time taken by each max-flow problem,which,in turn,depends on the number of augmenting paths that need to be computed. For the case of Fast-PD,the number of augmentations per inner-iteration decreases dramatically,as the algorithm progresses.E.g.Fast-PD has been applied to the problem of image restoration,andfig.7contains a related result about the denoising of a corrupted(with gaussian noise)“pen-guin”image(256labels and a truncated quadratic distance d(a,b)=min(|a−b|2,D)-where D=200-has been used in this case).Also,fig.8(a)shows the corresponding num-ber of augmenting paths per outer-iteration(i.e.per group of|L|inner-iterations).Notice that,for bothα-expansion, as well as PD3a,this number remains very high(i.e.almost over2·106paths)throughout all iterations.On the contrary, for the case of Fast-PD,it drops towards zero very quickly, e.g.only4905and7paths had to be found during the 8th and last outer-iteration respectively(obviously,as also shown in Fig.9(a),this directly affects the total time needed per outer-iteration).In fact,for the case of Fast-PD,it is very typical that,after very few inner-iterations,no more than10or20augmenting paths need to be computed per max-flow,which really boosts the performance in this case.This property can be explained by the fact that Fast-PD maintains both a primal,as well as a dual solution through-out its execution.Fast-PD then manages to effectively use the dual solutions of previous inner iterations,so as to re-duce the number of augmenting paths for the next inner-iterations.Intuitively,what happens is that Fast-PD ulti-mately wants to close the gap between the primal and the(a)High-level view of the Fast-PD algorithm(b)High-level view of theα-expansion algorithmFig.6:(a)Fast-PD generates pairs of primal-dual solutions iter-atively,with the goal of always reducing the primal-dual gap(i.e.the gap between the resulting primal and dual costs).But,for thecase of Fast-PD,this gap can be viewed as a rough estimate for thenumber of augmentations,and so this number is forced to reduceover time as well.(b)On the contrary,α-expansion works onlyin the primal domain(i.e.it is as if afixed dual cost is used at thestart of each new iteration)and thus the primal-dual gap can neverbecome small enough.Therefore,no significant reduction in thenumber of augmentations takes place as the algorithm progresses. dual cost(see Theorem1),and,for this,it iteratively gener-ates primal-dual pairs,with the goal of decreasing the size of this gap(see Fig.6(a)).But,for Fast-PD,the gap’s sizecan be thought of as,roughly speaking,an upper-bound for the number of augmenting paths per inner-iteration.Since,furthermore,Fast-PD manages to reduce this gap at anytime throughout its execution,the number of augmenting paths is forced to decrease over time as well.On the contrary,a method likeα-expansion,thatworks only in the primal domain,ignores dual solutions completely.It is,roughly speaking,as ifα-expansionis resetting the dual solution to zero at the start of each inner-iteration,thus effectively forgetting that solutionthereafter(see Fig.6(b)).For this reason,it fails toreduce the primal-dual gap and thus also fails to achieve a reduction in path augmentations over time,i.e.across inner-iterations.But the PD3a algorithm as well fails to mimicFast-PD’s behavior(despite being a primal-dual method). As explained in sec.3,this happens because,in this case, PREEDIT DUAL temporarily destroy the gap just before the start of UPDATE PRIMALS,i.e.just before max-flow is about to begin computing theaugmenting paths.(Note,of course,that this destruction is only temporary,and the gap is restored again after the execution of UPDATE PRIMALS).The above mentioned relationship between primal-dual gap and number of augmenting paths is formally described in the next theorem(see[1]for a complete proof): Theorem4.For Fast-PD,the primal-dual gap at the cur-rent inner-iteration forms an approximate upper bound for the number of augmenting paths at each iteration thereafter. Sketch of proof.During a c-iteration,it can be shown that dual-cost≤ p min(h p(c),h p(x p)),whereas primal-cost= p h p(x p),and so the primal-dual gap upper-bounds the following quantity: p[h p(x p)−h p(c)]+= p cap s p.Fig.7:Left:“Tsukuba”image and its disparity by Fast-PD.Mid-dle:a“SRI tree”image and corresponding disparity by Fast-PD. Right:noisy“penguin”image and its restoration by Fast-PD. But this quantity obviously forms an upper-bound on the maximumflow,which,in turn,upper-bounds the number of augmentations(assuming integralflows).Due to the above mentioned property,the time per outer-iteration decreases dramatically over time.This has been verified experimentally with virtually all problems that Fast-PD has been tested on. E.g.Fast-PD has been also applied to the problem of stereo matching,andfig. 7contains the resulting disparity(of size384×288with 16labels)for the well-known“Tsukuba”stereo pair,as well as the resulting disparity(of size256×233with 10labels)for an image pair from the well-known“SRI tree”sequence(in both cases,a truncated linear distance d(a,b)=min(|a−b|,D)-with D=2and D=5-has been used,while the weights w pq were allowed to vary based on the image gradient at p).Figures9(b),9(c)contain the corresponding running times per outer iteration.Notice how much faster the outer-iterations of Fast-PD become as the algorithm progresses,e.g.the last outer-iteration of Fast-PD(for the“SRI-tree”example)lasted less than1 msec(since,as it turns out,only4augmenting paths had to be found during that iteration).Contrast this with the behavior of either theα-expansion or the PD3a algorithm, which both require an almost constant amount of time per outer-iteration,e.g.the last outer-iteration ofα-expansion needed more than0.4secs tofinish(i.e.it was more than 400times slower than Fast-PD’s iteration!).Similarly,for the“Tsukuba”example,α-expansion’s last outer-iteration was more than2000times slower than Fast-PD’s iteration.Max-flow algorithm adaptation:However,for fully exploiting the decreasing number of path augmentations and reduce the running time,we had to properly adapt the max-flow algorithm.To this end,the crucial thing to observe was that the decreasing number of augmentations was directly related to the decreasing number of s-linked nodes,as already explained in sec.3.E.g.fig.8(b)shows how the number of s-linked nodes varies per outer-iteration for the“penguin”example(with a similar behavior being observed for the other examples as well).As can be seen, this number decreases drastically over time.In fact,asstart growing by exploring non-saturated edges that are adjacent to s-linked nodes,whereas the sink tree will grow starting from all t-linked nodes.Of course,the algorithm terminates when no adjacent unsaturated edges can be found any more.However,in our case,maintaining the sink tree is completely inefficient and does not exploit the much smaller number of s-linked nodes.We thus propose maintaining only the source tree during max-flow,which will be a much cheaper thing to do here(e.g.,in many inner iterations,there can be fewer than10s-linked nodes,but many thousands of t-linked nodes).Moreover,due to the small size of the source tree,detecting the termination of the max-flow procedure can now be done a lot faster,i.e.with-Fig. andcorresponding solutions have become almost optimal very early. out having to fully expand the large sink tree(which is a very costly operation),thus giving a substantial speedup.In addition to that,for efficiently building the source tree,we keep track of all s-linked nodes and don’t recompute them from scratch each time.In our case,this tracking can be done without cost,since,as explained in sec.3,an s-linked node can be created only inside the PREEDITDUALS routine,and thus can be easily detected. The above simple strategy has been extremely effective for boosting the performance of max-flow,especially when a small number of augmentations were needed.Incremental graph construction:But besides the max-flow algorithm adaptation,we may also modify the way graph G c is constructed.I.e.instead of constructing the ca-pacitated graph G c from scratch each time,we also propose an incremental way of setting its capacities.The following lemma turns out to be crucial in this regard:Lemma1.Let G c,¯G c be the graphs for the current and previous c-iteration.Let also p,q be2neighboring MRF nodes.If,during the interval from the previous to the cur-rent c-iteration,no change of label took place for p and q, then the capacities of the interior edges pq,qp in G c and of the exterior edges s p,p t,s q,q t in G c equal the residual capacities of the corresponding edges in¯G c.The proof follows directly from the fact that if no change of label took place for p,q,then none of the height variables h p(x p),h q(x q)or the balance variables y pq(x p),y qp(x q) could have changed.Due to lemma1,for building graph G c, we can simply reuse the residual graph of¯G c and only re-compute those capacities of G c for which the above lemma does not hold,thus speeding-up the algorithm even further.Combining speed with optimality:Fig.9(d)contains the running times of Fast-PD for various MRF problems. As can be seen from thatfigure,Fast-PD proves to be much faster than either theα-expansion6or the PD3a method,e.g. Fast-PD has been more than9times faster thanα-expansion for the case of the“penguin”image(17.44secs vs173.1 secs).In fact,this behavior is a typical one,since Fast-PD has consistently provided at least a3-9times speedup for all the problems it has been tested on.However,besides its efficiency,Fast-PD does not make any compromise re-garding the optimality of its solutions.On one hand,this is ensured by theorems2,3.On the other hand,Fast-PD,like cost,since any ratio between the cost of a primal solution and the cost of a dual solution can form such a bound.E.g.fig.10shows how these ratios vary per inner-iteration for the“tsukuba”and“penguin”problems(with similar results holding for the other problems as well).As one can notice, these ratios drop to1very quickly,meaning that an almost optimal solution has already been estimated even after justa few iterations(and despite the problem being NP-hard).5.Dynamic MRFsBut,besides single MRFs,Fast-PD can be easily adapted to also boost the efficiency for dynamic MRFs[5],i.e. MRFs varying over time,thus showing the generality and power of the proposed method.In fact,Fast-PDfits per-fectly to this task.The implicit assumption here is that the change between successive MRFs is small,and so,by ini-tializing the current MRF with thefinal(primal)solution of the previous MRF,one expects to speed up inference.A sig-nificant advantage of Fast-PD in this regard,however,is that it can exploit not only previous MRF’s primal solution(say ¯x),but also its dual solution(say¯y).And this,for initializ-ing current MRF’s both primal and dual solutions(say x,y).Obviously,for initializing x,one can simply set x=¯x. Regarding the initialization of y,however,things are slightly more complicated.For maintaining Fast-PD’s optimality properties,it turns out that,after setting y=¯y, a slight correction still needs to be applied to y.In particular,Fast-PD requires its initial solution y to satisfy condition(4),i.e.y pq(x p)+y qp(x q)=w pq d(x p,x q), whereas¯y satisfies¯y pq(x p)+¯y qp(x q)=¯w pq¯d(x p,x q), i.e.condition(4)with w pq d(·,·)replaced by the pairwise potential¯w pq¯d(·,·)of the previous MRF.The solution forfixing that is very simple: e.g.we can simply set y pq(x p)+=w pq d(x p,x q)−¯w pq¯d(x p,x q).Finally,for tak-ing into account the possibly different singleton potentials between successive MRFs,the new heights will obviously need to be updated as h p(·)+=c p(·)−c p(·)are the singleton potentials of the previous MRF.These are the only changes needed for the case of dynamic MRFs,and thus the new pseudocode appears in Fig.11.As expected,for dynamic MRFs,the speedup provided by Fast-PD is even greater than single MRFs. E.g.Fig. 12(a)shows the running times per frame for the“SRI tree”image sequence.Fast-PD proves to be be more than10 times faster thanα-expansion in this case(requiring on average0.22secs per frame,whereasα-expansion required 2.28secs on average).Fast-PD can thus run on about5。

Curriculum VitaeProfessor Shaher MomaniDepartment of Mathematics,Mutah UniversityP.O.Box7,Al-Karak,Jordan.Mobile:+962(0)777500326E-mail:shahermm@Web Site:.jo/userhomepages/shmomani/index.htmWeb Site:.jo/jrgam/index.htmlPersonal Data•Full Name:Shaher Mohammad Ahmad Momani•Date of Birth:May10,1962•Place of Birth:Ajloun-Jordan•Nationality:Jordanian•Sex:Male•Marital Status:Married,two daughters and two sons•Profession:Professor of Mathematics at Mutah UniversityAcademic Qualification•Ph.D.in Mathematics,Applied Mathematics(Non-Newtonian Fluid Mechanics) University:University:of Wales,United Kingdom,1991.Title of Thesis:Some Problems in Non-Newtonian Fluid Mechanics.Advisor:Professor Ken Walters.•B.Sc.in MathematicsUniversity:Yarmouk University,Jordan,1984.Experience•Editor-in-Chief:Arab Journal Of Mathematics And Mathematical Sciences(AJMMS).Web Site:•Leader of Jordan Research Group in Applied Mathematics(JRGAM).Web Site:.jo/jrgam/index.html•Professor:Mutah University,September20067to present.1•Professor:Qatar University,September2006to September2007.•Associate Professor:Mutah University,September2004to September2006.•Associate Professor:Jordan University,Summer course2004.•Associate Professor:United Arab Emirates University,September2001to September2004.•Associate Professor:Yarmouk University,September2000to September2001.•Associate Professor:Mutah University,November1998to September2000.•Assistant Professor:Mutah University,September1991to November1998.•Head of Department of Mathematics,Mutah University,September1994to September1995.•Visiting Professor:Department of Mathematics,University of Wales,June-August1996,UK. Research InterestsMy general research interests are in the areas of applied mathematics,Non-Newtonian Fluid Mechanics, differential equations of applied mathematics,fractional calculus and fractional differential equation. More specifically,my research interests can be summarized as follows:1.Numerical solution of ordinary and partial differential equations of fractional order.2.Theory of fractional differential equations and integral equations.3.Newtonian and Non-Newtonianfluid mechanics.4.Stability of fractional linear systems.5.Fractional chaotic systems.6.Variational inequalities and obstacle problems.7.Mathematical Modelling.8.Mathematical Physics.9.Solitary Waves.10.Oil Shales.Editor1.Arab Journal of Mathematics and Mathematical Sciences,(Editor-in-Chief).2.International Journal of Nonlinear Dynamical Systems and Chaos(IJNDSC).3.Journal of Fractional Calculus and Its Applications.4.International Journal of Computational Mathematics and Numerical Simulation(IJCMNS).5.Journal of Nonlinear and Fractional Phenomena in Science and Engineering.6.International Review of Pure and Applied Physics.7.Mutah Journal for Scientific Research.2Reviewer•Journal of Computational and applied Mathematics.•Journal of Mathematical Analysis and Applications.•Physics Letters A.•Physica Scripta.•Electronic Journal of Differential Equations.•Communications in Nonlinear Science and Numerical Simulation.•Chaos,Solitons&Fractals.•Journal of Applied Analysis.•Arabian Journal for Science and Engineering.•Computers and Mathematics with Applications.•International Journal of Computer Mathematics.•Journal of Applied Mathematics.•International Journal of Mathematics and Mathematical Sciences.•Numerical Methods for Partial Differential Equations.•Referee for several international and local journals.Membership1.Member of the International Who’s Who,since2006.2.Member of the Jordanian Mathematics Society,since1991.3.Member of the Exactive Committee of the Jordanian Mathematics Society,1994-1996.4.Member of the British Society of Rheology,since1989.5.Member of Newton Institute of Non-Newtonian Fluid Mechanics.University of Wales.6.Member of the American Mathematical Society,since1996.7.Leader of Jordan Research Group in Applied Mathematics(JRGAM),Jordan,2005−Present.8.Member of the fractional calculus and its applications cuminuty.http:http://www.tuke.sk/podlubny/fc.html9.Member of the Research Group in Mathematical Inequalities and Applications(RGMIA). Academic Honors and Grants1.Third World Academy of Sciences(TWAS)prize,in Italy,(2000).2.A Scholarship from Mutah University to get a PhD(1987-1991).3.A Grant from Qatar University to do a Research Project on Chaotic Dynamics and Phase Syn-chronization of Fractional Order Dynamical Systems(2007-2008).3Some of my Co-workers1.Professor Ishak Hashim,School of Mathematical Sciences,University Kebangsaan Malaysia.2.Professor Shijun Liao,Shanghai Jiao Tong University,China.3.Professor Hossain Erjaee,University of Qatar,Qatar.4.Professor Nabil Shawagfeh,University of Jordan,Jordan.5.Professor S.B.Hadid,Ajman University for Science and Technology,UAE.6.Professor Ahamed Alawaneh,University of Jordan,Jordan.7.Professor Muhammad Aslam Noor,COMSTATS Institute of Information Tech.,Pakistan.8.Professor Dogan Kaya,Firat University,Turkey.9.Dr Kamel Al-Khaled,Jordan University of Science and Tech.,Jordan.10.Dr Reyad Al-Khazali,Etisalat College,UAE.11.Dr Zaid Odibat,Al-Balq’a University,Jordan.12.Dr Hossein Jafari,Mazandaran University,Babolsar,Iran.13.Dr Vedat Suat Erturk,Department of Mathematics,Ondokuz Mayis University,Turkey.14.Dr Rabha Ibrahim,Sana’a,Yemen.Committee Service•Mutah University1.Member of the Organizing Committee for the2nd Jordanian Mathematics Conference,1994.2.Member of the Organizing Committee for the3rd Jordanian Mathematics Conference,1996.3.Member of the Organizing Committee for A Workshop in Teaching Calculus Using Mathe-matica Software,Mutah Univ.,1996.4.Member of a Committee to Study the Academic Status at Mutah Univ.5.Member of the Housing Committee1995-1996.6.Member of the Library Committee1995-1996.7.Member of the Supervising Committee of Mutah Univ.School1995-1997.8.Member of Several Internal Committees in the Faculty and Department.9.Head of the Committee for Establishing the Master Program at Mutah University,2000.10.Member of the Seminar Committee2005-present.11.Member of the Graduate Studies Committee2005-present.12.Member of the Appointing Committee of Mutah Univ.School2005.13.Member of Several Internal Committees in the Faculty and Department.14.Member of Several Committees at Mutah University during the academic years2004-2006.15.Coordinator and Member of Several Committees at Mutah University during the academicyears2007-present.4•Yarmouk University1.Member of the Scientific Research Committee.2.Member of Several Internal Committees in the Faculty and Department.•United Arab Emirates University1.Coordinator of the Practical Training and Field Trips Committee.2.Coordinator of the Counseling and Advising Committee.3.Member of the Cultural and Social Committee.4.Member of the Information and Annual Report Committee.5.Member of the Curricular Committee in the Faculty.6.Member of Several Internal Committees in the Faculty and Department.•Qatar University1.Coordinator and Member of Several Internal Committees in the Faculty and Department.•Outside Universities1.Member of the Committee for Maths.Department of Irbid Private Univ.2.Member of the Committee for Maths.Department of Zarqa Private Univ.3.Referee for Research Papers Publish in Various Journals.4.Member of a Defense exam Committee for Several Master Theses in Jordan Universities.5.Chaired a Session of the Third Jordanian Mathematics Conference,1996.6.Chaired a Session of the Fifth Annual U.A.E.University Conference,2004.7.Chaired a Session of the Recent Advances in Mathematics Conference,India,2004.8.Member of the Exactive Committee of Qualification Exam at Jordan Universities.9.Chaired a Session of The Third Conferences On Research And Education In Mathematics,Malaysia2007.10.Member of the Organizing Committee of The2nd International Symposium on NonlinearDynamics,Shanghai,China,2007.11.Chaired a Mini-Symposium in The2nd International Symposium on Nonlinear Dynamics,Shanghai,China,2007.12.Member of the International Program Committee of the Fractional Differentiation and itsApplications,Ankrah,Turkey,2008.Computer Skills1.Mathematical Software:Mathematica,Fortran,Maple,Matlab.2.Operating Systems:DOS,UNIX,Windows2000.3.Typesetting Software:Tex,LaTeX,Scientific Workplace,MicroSoft Word.4.MCDL:Mutah Computer Drive License.5Published and Accepted PapersThis is a complete list of the papers of mine which either have appeared or have been accepted for publication.Owing to copyright restrictions,the papers are not available in electronic form.If you are interested in any of these papers,send me an e-mail and I will send you a reprint.1.G.Georgiou,Shaher Momani,M.J.Crochet,and K.Walters,Newtonian and non-Newtonianflow in a channel obstructed by an antisymmetric array of cylinders,Journal of Non-Newtonian Fluid Mechanics,Vol.40,(1991)231-260.2.S.Hadid,B.Maseadeh and Shaher Momani,On the existence of maximal and minimalsolutions of differential equations of non-integer order,Journal of Fractional Calculus,Vol.9, (1996)41-44.3.S.B.Hadid, A.A.Ta’ani and S.M.Momani,Some existence theorems on differentialequations of generalized order through afixed-point theorem,Journal of Fractional Calculus,Vol.9,(1996)45-49.4.B.S.Maseadeh,A.A.Ta’ani and S.M.Momani,On w-compact spaces,J.of Institute ofMathematics and Computer Sciences,(1996).5.B.Maseadeh,S.Momani and S.Hadid,Solutions of differential equations of non-integerorder in L2and C spaces,Mutah Journal for Research and Studies,Vol.12(1),(1997)169-181.6.Shaher Momani,Theflow of non-Newtonianfluids through corrugated pipes,Mu’tah Journalfor Research and Studies,Vol.12(4),(1997)91-112.7.S.Momani and S.Hadid,An algorithm for numerical solutions of fractional order differentialequations,Journal of Fractional Calculus,Vol.15,(1998)61-66.8.S.M.Momani and K.Walters,Theflow of non-Newtonianfluids through curved pipes,Al-Dirasat Journal,Vol.26(1),(1999)74-87.9.S.M.Momani,On existence of solutions of a system of ordinary differential equations of frac-tional order,Far East Journal of Mathematical Sciences(FJMS),Vol.1(2),(1999)265-270. 10.S.M.Momani,Variation of solutions of differential equations of non-integer order with respectto initial condition and parameters,Far East Journal of Mathematical Sciences(FJMS),Vol.1(3),(1999)423-428.11.S.M.Momani,Stress distribution and pressure gradient of non-Newtonianfluids through con-verging ducts,Mu’tah Lil-Buhooth Wa Al-Dirasat Journal,Vol.15(1),(2000)9-26.12.S.M.Momani,Local and global uniqueness theorems on differential equations of non-integerorder via Gronwall’s and Bihari’s inequalities,Revista Technica Journal,Vol.23(1),(2000)66-69.13.Shaher Momani,Numerical solution of differential equations of non-integer order by the gener-alized difference method,Al-Zarqa Private University Journal,Vol.2(1),(2000)1-7.14.S.M.Momani,On the existence ofε-approximate solutions of differential equations of non-integer order,PanAmerican Mathematical Journal,Vol.10(3),(2000)61-69.15.Shaher M.Momani,Local and global existence theorems on fractional integro-differential equa-tions,Journal of Fractional Calculus,Vol.18,(2000)81-86.16.Shaher M.Momani and Reyad El-Khazali,On the existence of extremal solutions of frac-tional integro-differential equations,Journal of Fractional Calculus,Vol.18,(2000)87-92.617.S.M.Momani,Theflow of non-Newtonianfluids through rotating pipes,Al-Manara Journal,Vol.7(1)(2001),9-25.18.Shaher Momani,Some existence theorems on fractional integro-differential equations,AbhathAl-Yarmouk Journal,Vol.10(2B),(2001)435-444.19.S.M.Momani and S.B.Hadid,Asymptotic behaviour of the maximal and minimal solutionsof differential equations of non-integer order,Far East Journal of Mathematical Sciences(FJMS), Vol.6(1),(2002)31-39.20.S.M.Momani and S.B.Hadid,Dependence of solutions of differential equations of non-integer order on initial conditions and parameters,Al-Manara Journal,Vol.9(2),(2003)69-76.21.Reyad El-Khazali,Shaher Momani,Stability analysis of composite fractional systems,In-ternational Journal of Applied Mathematics,Vol.12(1),(2003)73-85.22.S.M.Momani and S.B.Hadid,On the inequalities of integro-differential fractional equations,International Journal of Applied Mathematics,Vol.12(1),(2003)29-37.23.S.M.Momani and S.B.Hadid,Some comparison results for integro-fractional differentialinequalities,Journal of Fractional Calculus,Vol.24,(2003)37-44.24.S.M.Momani,S.B.Hadid and Z.M.Alawaneh,Some analytical properties of solutionsof differential equations of the noninteger order,International Journal of Mathematics and Math-ematical Sciences,Vol.2004(13),(2004)697-701.25.Shaher Momani,Analytical solutions of strongly non-linear oscillators by the decompositionmethod,International Journal of Modern Physics C(IJMPC),Vol.15(7),(2004)967-979.26.Shaher Momani and Samir Hadid,Lyapunov stability solutions of fractional integro-differential equations,International Journal of Mathematics and Mathematical Sciences,Vol.2004(47),(2004)2503-2507.27.Shaher Momani and Kamel Al-Khaled,Numerical solutions for systems of fractional dif-ferential equations by the decomposition method,Applied Mathematics and Computation,Vol.162(3),(2005)1351-1365.28.S.M.Momani and S. B.Hadid,On the continuous dependence of solutions of integro-fractional differential equations with respect to initial conditions,Nonlinear Functional Analysis and Applications,Vol.10(3),(2005)379-386.29.Kamel Al-Khaled and Shaher Momani,An approximate solution for a fractional diffusion-wave equation using the decomposition method,Applied Mathematics and Computation,Vol.165(2),(2005)473-483.30.Shaher Momani,Analytical approximate solution for fractional heat-like and wave-like equa-tions with variable coefficients using the decomposition method,Applied Mathematics and Com-putation,Vol.165(2),(2005)459-472.31.Shaher Momani,Khaled Moadi and Muhammad Aslam Noor,Modified decompositionmethod for solving a system of third-order obstacle problems,International Journal of Pure and Applied Mathematics,Vol.21(1),(2005)97-107.32.Shaher Momani,An explicit and numerical solutions of the fractional KdV equation,Mathe-matics and Computers in Simulation,Vol.70(2),(2005)110-118.733.Shaher Momani,A numerical scheme for the solution of Sivashinsky equation,Applied Mathe-matics and Computation,Vol.168(2),(2005)1273-1280.34.Shaher Momani,Analytic and approximate solutions of the space-and time-fractional telegraphequations,Applied Mathematics and Computation,Vol.170(2),(2005)1126-1134.35.Kamel Al-Khaled,Shaher Momani and Ahmed Alawneh,Approximate wave solutions fora generalized Benjamin-Bona-Mahoy-Burgers equation,Applied Mathematics and Computation,Vol.171(1),(2005)281-292.36.Muhammad Aslam Noor,S.K.Mishra and Shaher Momani,Properties of approximatepreinvex functions,Nonlinear Analysis Forum Journal,Vol.10(2),(2005)1-9.37.Shaher Momani and Salah Abuasad,Application of He’s variational iteration method toHelmholtz equation,Chaos,Solitons&Fractals,Vol.27(5),(2006)1119-1123.38.Zaid Odibat and Shaher Momani,Application of variational iteration method to nonlineardifferential equations of fractional order,International Journal of Nonlinear Science and Numer-ical Simulation,Vol.7(1),(2006)27-34.39.Shaher Momani,Non-perturbative analytical solutions of the space-and time-fractional Burgersequations,Chaos,Solitons&Fractals,Vol.28(4),(2006)930-937.40.Shaher Momani,Khaled Moadi and Muhammad Aslam Noor,Decomposition methodfor solving fourth order obstacle problems,Applied Mathematics and Computation,Vol.175(2), (2006)923-931.41.Shaher Momani,Solving a system of second-order obstacle problems a modified decompositionmethod,Applied Mathematics E-Notes,Vol.6,(2006)141-147.42.Shaher Momani and Zaid Odibat,Analytical approach to linear fractional partial differentialequations arising influid mechanics,Physics Letters A,Vol.355,(2006)271-279.43.Shaher Momani and Zaid Odibat,Analytical solution of a time-fractional Navier-Stokes equa-tion by Adomian decomposition method,Applied Mathematics and Computation,Vol.177,(2006) 488-494.44.Shaher Momani and Khaled Moadi,A reliable algorithm for solving fourth-order boundaryvalue problems,Journal of Applied Mathematics and Computing,Vol.22(3),(2006)185-197. 45.Ziad Odibat and Shaher Momani,Approximate solutions for boundary value problems oftime-fractional wave equation,Applied Mathematics and Computation,Vol.181(1),(2006)767-774.46.Shaher Momani and Rami Qaralleh,An efficient method for solving systems of fractionalintegro-differential equations,Computers and Mathematics with Application,Vol.52(3-4),(2006) 459-470.47.Ziad Odibat and Shaher Momani,Analytical spherically symmetric solution for the time-fractional Navier-Stokes equation,Advances in Theoretical and Apllied Mathematics(ATAM), Vol.1(2),(2006)97-107.48.Shaher Momani and Muhammad Aslam Noor,Numerical methods for fourth-order frac-tional integro-differential equations,Applied Mathematics and Computation,Vol.182(1),(2006) 754-760.849.Shaher Momani,A numerical scheme for the solution of multi-order fractional differential equa-tions,Applied Mathematics and Computation,Vol.182(1),(2006)761-770.50.Shaher Momani and Nabil Shawagfeh,Decomposition method for solving the fractionalRiccati differential equation,Applied Mathematics and Computation,Vol.182(2),(2006)1083-1092.51.Shaher Momani and Rami Qaralleh,Analytical approximate solution for a nonlinear frac-tional integro-differential equation,Nonlinear Analysis Forum Journal,Vol.11(2),(2006)237-249.52.Shaher Momani,Salah Abuasad and Zaid Odibat,Variational iteration method for solvingnon-linear boundary value problems,Applied Mathematics and Computation,Vol.183,(2006) 1351-1358.53.Shaher Momani,General solutions for the space-and time-fractional diffusion-wave equation,Journal of Physical Sciences,Vol.10,(2006)30-43.54.Shaher Momani and Zaid Odibat,Numerical comparison of methods for solving linear dif-ferential equations of fractional order,Chaos,Solitons&Fractals,Vol.31(5),(2007)1248-1255.55.Shaher Momani,An algorithm for solving a nonlinear fractional convection-diffusion problem,Communications in Nonlinear Science and Numerical Simulation,Vol.12(7),(2007)1283-1290.56.Shaher Momani and Zaid Odibat,Numerical approach to differential equations of fractionalorder,Journal of Computational and Applied Mathematics,Vol.207(1),(2007)96-110.57.Shaher Momani and Zaid Odibat,Fractional Green’s function for linear fractional inhomo-geneous partial differential equations influid mechanics,Journal of Applied Mathematics and Computing,Vol.24,(2007)167-178.58.Shaher Momani and Rami Qaralleh,Numerical approximations and Pade approximants fora fractional population growth model,Applied Mathematical Modelling,Vol.31(9),(2007)1907-1914.59.Shaher Momani and Ziad Odibat,Comparison between homotopy perturbation method andthe variational iteration method for linear fractional partial differential equations,Computers and Mathematics with Applications,Vol.54,(2007)910-919.60.Vedat Suat Erturk and Shaher Momani,Comparing numerical method for solving fourth-order boundary value problems,Applied Mathematics and Computation,Vol.188,(2007)1963-1968.61.Rabha Ibrahim and Shaher Momani,On the existence and uniqueness of solutions of aclass of fractional differential equations,Journal of Mathematical Analysis and Applications,Vol.334(1),(2007)1-10.62.Shaher Momani and Ziad Odibat,Homotopy perturbation method for nonlinear partial dif-ferential equations of fractional order,Physics Letters A,Vol.365,(2007)345-350.63.Zaid Odibat and Shaher Momani,A reliable treatment of homotopy perturbation methodfor Klein-Gordon equations,Physics Letters A,Vol.365,(2007)351-357.64.Khalida Inayat Noor,Muhammad Aslam Noor and Shaher Momani,Modified House-holder iterative method for nonlinear equations,Applied Mathematics and Computation,Vol.190, (2007)1534-1539.965.Shaher Momani and Muhammad Aslam Noor,Numerical comparison of methods for solv-ing a special fourth-order boundary value problem,Applied Mathematics and Computation,Vol.191,(2007)218-224.66.Rabha Ibrahim and Shaher Momani,Multiple solutions for multi-order fractional differentialequations,Arab Journal of Mathematics and Mathematical Sciences,Vol.1,(2007)28-34.67.Shaher Momani,A decomposition method for solving unsteady convection-diffusion problems,Turkish Journal of Mathematics,Vol.31,(2007)1-10.68.Vedat Suat Erturk and Shaher Momani,A reliable algorithm for solving tenth-order bound-ary value problems,Numerical Algorithms,Vol.44(2),(2007)147-158.69.Zaid Odibat and Shaher Momani,Numerical solution of Fokker-Planck equation with space-and time-fractional derivtives,Physics Letters A,Vol.369(2007),349-358.70.Shaher Momani,Zaid Odibat and Vedat Suat Erturk,Generalized differential transformmethod for solving a space-and time-fractional diffusion-wave equation,Physics Letters A,Vol.370,(2007)379-387.71.Hossien Jafari and Shaher Momani,Solving fractional diffusion and wave equations by mod-ified homotopy perturbation method,Physics Letters A,Vol.370,(2007)388-396.72.Zaid Odibat and Shaher Momani,Numerical methods for nonlinear partial differential equa-tions of fractional order,Applied Mathematical modlling,Vol.32,(2008)28-39.73.Shaher Momani and Rabha Ibrahim,On a fractional integral equation of periodic func-tions involving Weyl-Riesz operator in Banach algebras,Journal of Mathematical Analysis and Applications,Vol.339,(2008)1210-1219.74.Zaid Odibat and Shaher Momani,Modified homotopy perturbation method:application toquadratic Riccati differential equation of fractional order,Chaos,Solitons&Fractals,Vol.36, (2008)167-174.75.Zaid Odibat and Shaher Momani,A generalized differential transform method for linearpartial differential equations of fractional order,Applied Mathematics Letters,Vol.21,(2008) 194-199.76.Shaher Momani and Ziad Odibat,A novel method for nonlinear fractional partial differentialequations:Combination of DTM and generalized Taylor’s formula,Journal of Computational and Applied Mathematics,accepted(2007),doi:10.1016/j.cam.2007.07.033.77.G.H.Erjaee and Shaher Momani,Phase synchronization in fractional differential chaoticsystems.Physics Letters A,accepted(2007),doi:10.1016/j.cam.2007.07.033.78.Vedat Suat Erturk Shaher Momani,and Zaid Odibat,Application of generalized dif-ferential transform method to multi-order fractional differential equations,Communications in Nonlinear Science and Numerical Simulation,accepted(2007),doi:10.1016/sns.2007.02.006.79.Vedat Suat Erturk and Shaher Momani,Solving systems of fractional differential equationsusing differential transform method,Journal of Computational and Applied Mathematics,accepted (2007),doi:10.1016/j.cam.2007.03.029.80.Shaher Momani and Vedat Suat Erturk,Solutions of non-linear oscillators by the modifieddifferential transform method,Computers&Mathematics with Applications,accepted(2007), doi:10.1016/j.camwa.2007.05.009.1081.M.S.Chowdhury,Ishak Hashim and Shaher Momani,The multistage homotopy-perturbation method:A powerful scheme for handling the Lorenz system.Chaos,Solitons& Fractals,accepted(2007),doi:10.1016/j.chaos.2007.09.073.82.Omar Abdulaziz,Ishak Hashim and Shaher Momani,Application of homotopy-perturbation method to fractional IVPs,Journal of Computational and Applied Mathematics, accepted(2007),doi:10.1016/j.cam.2007.06.010.83.Omar Abdulaziz,Ishak Hashim and Shaher Momani,Solving systems of fractional dif-ferential equations by homotopy-perturbation method.Physics Letters A,accepted(2007), doi:10.1016/j.physleta.2007.07.059.84.Zaid Odibat,Shaher Momani and Vedat Suat Erturk,Generalized differential transformmethod:Application to differential equations of fractional order.Applied Mathematics and Com-putation,Vol.372(4),(2008)451-459.85.Omar Jaradat,Ahmad Al-Omari and Shaher Momani,Exsitence of the mild solutionfor fractional semilinear initial value problems,Nonlinear Analysis Journal:Theory,Methods& Applications,accepted(2007),doi:10.1016/j.na.2007.09.008.86.Ishak Hashim,Omar Abdulaziz and Shaher Momani,Homotopy analysis method for frac-tional IVPs,Communications in Nonlinear Science and Numerical Simulation,accepted(2007), doi:10.1016/sns.2007.09.014.87.Shaher Momani,Ziad Odibat and Ahmed Alawneh,Variational iteration method for solv-ing the space-and time-fractional KdV equation,Numerical Methods for Partial Differential Equations Journal,accepted(2007),doi:10.1002/num.20247.88.Shaher Momani and Vedat Suat Erturk,A numerical scheme for the solution of viscousCahn-Hilliard equation,Numerical Methods for Partial Differential Equations Journal,accepted (2007),doi:10.1002/num.20286.89.Shaher Momani and Ziad Odibat,Numerical solutions of the space-time fractional advection-dispersion equation,Numerical Methods for Partial Differential Equations Journal,accepted (2007),doi10.1002/num.20324.90.Zaid Odibat and Shaher Momani,Analytical comparison between the homotopy perturbationmethod and variational iteration method for differential equations of fractional order,International Journal of Modern Physics B,accepted(2007).91.Shaher Momani and Vedat Suat Erturk,Solving a system of fourth-order obstacle boundaryvalue problems by differential transform method,Kybernetes,(2007).92.Shaher Momani,Omar Jaradat and Rabha Ibrahim,Numerical approximations of a dy-namic system containing fractional derivatives.Journal of Applied Sciences,accepted(2008). 93.Shaher Momani and Hossein Jafari,Numerical study of systems of fractional differentialequations by the decomposition method.Southeast Asian Bulletin of Mathematics,accepted (2006).94.S.M.Momani,Ahlam Jameel and Sora Al-Azwai,Local and global uniqueness theoremson fractional integro-differential equations via Gronwall’s and Bihari’s inequalities.Soochow Jour-nal of Mathematics,Vol.33(4),(2007)619-627.95.Vedat Suat Erturk and Shaher Momani,Differential transform technique for solvingfifth-order boundary value problems.Indian Journal of Pure and Applied Mathematics,accepted (2007).1196.Zaid Odibat and Shaher Momani,An algorithm for the numerical solution of differentialequations of fractional order,Journal of Applied Mathematics and Informatics,accepted(2007).97.Shaher Momani,Numerical simulations for the space-and time-fractional partial differentialequations,Proceedings of The Third Conferences On Research And Education In Mathematics, Malaysia,(2007)51-56.98.Vedat Suat Erturk and Shaher Momani,Differential transform method for obtaining posi-tive solutions for two-point nonlinear boundary value problems,International Conference:2007 Dynamical Systems and Applications,July1-6,2007,Izmir,Turkey,accepted.99.Shaher Momani,Ziad Odibat and Ishak Hasim,Algorithms for nonlinear fractional partialdifferential equations:A selection of numerical methods,The2nd International Symposium on Nonlinear Dynamics,27-30Oct.,2007,Shanghai,China,accepted.100.Zaid Odibat,Shaher Momani and Ahmed Alawneh,Analytic study on time-fractional Schr¨o dinger equations:Exact solutions by GDTM,The2nd International Symposium on Nonlin-ear Dynamics,27-30Oct.,2007,Shanghai,China,accepted.101.Zaid Odibat,Shaher Momani,Applications of variational iteration and homotopy perturba-tion methods to fractional evolution equations,The2nd International Symposium on Nonlinear Dynamics,27-30Oct.,2007,Shanghai,China,accepted.102.Shaher Momani,An efficient numerical scheme for solving fractional convection-diffusion prob-lems.International Journal of Computational and Numerical Analysis and Applications,accepted (2007).103.Ziad Odibat,Shaher Momani and Ahmed Alawneh,Approximate analytical solution of the space-and time-fractional Burgers equations.Journal Europ´e en des Syst´e mes Automatis´e s, accepted.104.Shaher Momani and Rabha Ibrahim,Analytical solutions of a fractional oscillator by the decomposition method,International Journal of Pure and Applied Mathematics,Vol.37(1), (2007)119-132.105.M.H.Alnasr and Shaher Momani,Application of homotopy perturbation method to singu-larly perturbed Volterra integral equations.Journal of Applied Sciences,accepted.106.Ziad Odibat and Shaher Momani,Fractional Green’s Function for a Class of Fractional Partial Differential Equations.Journal Europ´e en des Syst´e mes Automatis´e s,accepted. Submitted Papers1.Shaher Momani and Salah Abuasad,Variational iteration method for solving Fisher’s equa-munications in Nonlinear Science and Numerical Simulation,submitted.2.Zaid Odibat and Shaher Momani,An analytic treatment of linear inhomogeneous fractionalpartial differential equations influid mechanics.Australian&New Zealand Industrial and Applied Mathematics Journal(ANZIAM),submitted.3.Rabha Ibrahim and Shaher Momani,On a fractional integral equation of periodic functionsinvolving Weyl-Riesz operator.Kyngpook Mathematical Journal,submitted.4.Hamid A.Jalab,Shaher Momani and Rabha Ibrahim,Parametric stability of almost-periodic solutions for BAM neural networks without delays.Journal of Mathematical Analysis and Applications,submitted.12。