2 Search Results for "Zhou, Jianqi"

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.34
Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems

Authors: Amos Robinson and Alex Potanin

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Synchronous languages such as Lustre and Scade are used to implement safety-critical control systems; proving such programs correct and having the proved properties apply to the compiled code is therefore equally critical. We introduce Pipit, a small synchronous language embedded in F*, designed for verifying control systems and executing them in real-time. Pipit includes a verified translation to transition systems; by reusing F*’s existing proof automation, certain safety properties can be automatically proved by k-induction on the transition system. Pipit can also generate executable code in a subset of F* which is suitable for compilation and real-time execution on embedded devices. The executable code is deterministic and total and preserves the semantics of the original program.
Cite as

Amos Robinson and Alex Potanin. Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 34:1-34:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{robinson_et_al:LIPIcs.ECOOP.2024.34,
  author =	{Robinson, Amos and Potanin, Alex},
  title =	{{Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{34:1--34:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.34},
  URN =		{urn:nbn:de:0030-drops-208836},
  doi =		{10.4230/LIPIcs.ECOOP.2024.34},
  annote =	{Keywords: Lustre, streaming, reactive, verification}
}
Document
DOI: 10.4230/LIPIcs.ISAAC.2022.50
Parameterized Approximation Algorithms for TSP

Authors: Jianqi Zhou, Peihua Li, and Jiong Guo

Published in: LIPIcs, Volume 248, 33rd International Symposium on Algorithms and Computation (ISAAC 2022)

Abstract
We study the Traveling Salesman problem (TSP), where given a complete undirected graph G = (V,E) with n vertices and an edge cost function c:E↦R_{⩾0}, the goal is to find a minimum-cost cycle visiting every vertex exactly once. It is well-known that unless P = NP, TSP cannot be approximated in polynomial time within a factor of ρ(n) for any computable function ρ, while the metric case of TSP, that the edge cost function satisfies the △-inequality, admits a polynomial-time 1.5-approximation. We investigate TSP on general graphs from the perspective of parameterized approximability. A parameterized ρ-approximation algorithm returns a ρ-approximation solution in f(k)⋅|I|^O(1) time, where f is a computable function and k is a parameter of the input I. We introduce two parameters, which measure the distance of a given TSP-instance from the metric case, and achieve the following two results: - A 3-approximation algorithm for TSP in O((3k₁)! 8^k₁⋅ n²+n³) time, where k₁ is the number of triangles in which the edge costs violate the △-inequality. - A 3-approximation algorithm for TSP in O(n^O(k₂)) time and a (6k₂+9)-approximation algorithm for TSP in O(k₂^O(k₂)⋅n³) time, where k₂ is the minimum number of vertices, whose removal results in a metric graph. To our best knowledge, the above algorithms are the first non-trivial parameterized approximation algorithms for TSP on general graphs.
Cite as

Jianqi Zhou, Peihua Li, and Jiong Guo. Parameterized Approximation Algorithms for TSP. In 33rd International Symposium on Algorithms and Computation (ISAAC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 248, pp. 50:1-50:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{zhou_et_al:LIPIcs.ISAAC.2022.50,
  author =	{Zhou, Jianqi and Li, Peihua and Guo, Jiong},
  title =	{{Parameterized Approximation Algorithms for TSP}},
  booktitle =	{33rd International Symposium on Algorithms and Computation (ISAAC 2022)},
  pages =	{50:1--50:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-258-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{248},
  editor =	{Bae, Sang Won and Park, Heejin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2022.50},
  URN =		{urn:nbn:de:0030-drops-173358},
  doi =		{10.4230/LIPIcs.ISAAC.2022.50},
  annote =	{Keywords: FPT-approximation algorithms, the Traveling Salesman problem, the triangle inequality, fixed-parameter tractability, metric graphs}
}
  • Refine by Author
  • 1 Guo, Jiong
  • 1 Li, Peihua
  • 1 Potanin, Alex
  • 1 Robinson, Amos
  • 1 Zhou, Jianqi

  • Refine by Classification
  • 1 Computer systems organization → Real-time languages
  • 1 Software and its engineering → Specialized application languages
  • 1 Theory of computation → Approximation algorithms analysis
  • 1 Theory of computation → Graph algorithms analysis
  • 1 Theory of computation → Program verification

  • Refine by Keyword
  • 1 FPT-approximation algorithms
  • 1 Lustre
  • 1 fixed-parameter tractability
  • 1 metric graphs
  • 1 reactive
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2022
  • 1 2024

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact