ACM SIGLOG News · 2016 · 33 citations · 52 references
Circuit ComplexityReachability AnalysisComputational Complexity TheoryEngineeringReachability ProblemFormal MethodsVector Addition SystemsComputational ComplexityTime ComplexityComputer ScienceDiscrete MathematicsCombinatorial OptimizationComplexity30Th Symposium
The program of the 30th Symposium on Logic in Computer Science held in 2015 in Kyoto included two contributions on the computational complexity of the reachability problem for vector addition systems: Blondin, Finkel, Göller, Haase, and McKenzie [2015] attacked the problem by providing the first tight complexity bounds in the case of dimension 2 systems with states, while Leroux and Schmitz [2015] proved the first complexity upper bound in the general case. The purpose of this column is to present the main ideas behind these two results, and more generally survey the current state of affairs.
52
Richard M. Karp, Raymond E. Miller · Journal of Computer and System Sciences · 1969 · 978 citations
Proving termination with multiset orderings
Nachum Dershowitz, Zohar Manna · Communications of the ACM · 1979 · 532 citations · Full text
Reasoning about systems with many processes
Steven M. German, A. Prasad Sistla · Journal of the ACM · 1992 · 437 citations · Full text