4 Search Results for "Wu, Song"

Document
DOI: 10.4230/DagRep.12.1.1
Mobility Data Science (Dagstuhl Seminar 22021)

Authors: Mohamed Mokbel, Mahmoud Sakr, Li Xiong, Andreas Züfle, Jussara Almeida, Taylor Anderson, Walid Aref, Gennady Andrienko, Natalia Andrienko, Yang Cao, Sanjay Chawla, Reynold Cheng, Panos Chrysanthis, Xiqi Fei, Gabriel Ghinita, Anita Graser, Dimitrios Gunopulos, Christian Jensen, Joon-Sook Kim, Kyoung-Sook Kim, Peer Kröger, John Krumm, Johannes Lauer, Amr Magdy, Mario Nascimento, Siva Ravada, Matthias Renz, Dimitris Sacharidis, Cyrus Shahabi, Flora Salim, Mohamed Sarwat, Maxime Schoemans, Bettina Speckmann, Egemen Tanin, Yannis Theodoridis, Kristian Torp, Goce Trajcevski, Marc van Kreveld, Carola Wenk, Martin Werner, Raymond Wong, Song Wu, Jianqiu Xu, Moustafa Youssef, Demetris Zeinalipour, Mengxuan Zhang, and Esteban Zimányi

Published in: Dagstuhl Reports, Volume 12, Issue 1 (2022)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 22021 "Mobility Data Science". This seminar was held January 9-14, 2022, including 47 participants from industry and academia. The goal of this Dagstuhl Seminar was to create a new research community of mobility data science in which the whole is greater than the sum of its parts by bringing together established leaders as well as promising young researchers from all fields related to mobility data science. Specifically, this report summarizes the main results of the seminar by (1) defining Mobility Data Science as a research domain, (2) by sketching its agenda in the coming years, and by (3) building a mobility data science community. (1) Mobility data science is defined as spatiotemporal data that additionally captures the behavior of moving entities (human, vehicle, animal, etc.). To understand, explain, and predict behavior, we note that a strong collaboration with research in behavioral and social sciences is needed. (2) Future research directions for mobility data science described in this report include a) mobility data acquisition and privacy, b) mobility data management and analysis, and c) applications of mobility data science. (3) We identify opportunities towards building a mobility data science community, towards collaborations between academic and industry, and towards a mobility data science curriculum.
Cite as

Mohamed Mokbel, Mahmoud Sakr, Li Xiong, Andreas Züfle, Jussara Almeida, Taylor Anderson, Walid Aref, Gennady Andrienko, Natalia Andrienko, Yang Cao, Sanjay Chawla, Reynold Cheng, Panos Chrysanthis, Xiqi Fei, Gabriel Ghinita, Anita Graser, Dimitrios Gunopulos, Christian Jensen, Joon-Sook Kim, Kyoung-Sook Kim, Peer Kröger, John Krumm, Johannes Lauer, Amr Magdy, Mario Nascimento, Siva Ravada, Matthias Renz, Dimitris Sacharidis, Cyrus Shahabi, Flora Salim, Mohamed Sarwat, Maxime Schoemans, Bettina Speckmann, Egemen Tanin, Yannis Theodoridis, Kristian Torp, Goce Trajcevski, Marc van Kreveld, Carola Wenk, Martin Werner, Raymond Wong, Song Wu, Jianqiu Xu, Moustafa Youssef, Demetris Zeinalipour, Mengxuan Zhang, and Esteban Zimányi. Mobility Data Science (Dagstuhl Seminar 22021). In Dagstuhl Reports, Volume 12, Issue 1, pp. 1-34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{mokbel_et_al:DagRep.12.1.1,
  author =	{Mokbel, Mohamed and Sakr, Mahmoud and Xiong, Li and Z\"{u}fle, Andreas and Almeida, Jussara and Anderson, Taylor and Aref, Walid and Andrienko, Gennady and Andrienko, Natalia and Cao, Yang and Chawla, Sanjay and Cheng, Reynold and Chrysanthis, Panos and Fei, Xiqi and Ghinita, Gabriel and Graser, Anita and Gunopulos, Dimitrios and Jensen, Christian and Kim, Joon-Sook and Kim, Kyoung-Sook and Kr\"{o}ger, Peer and Krumm, John and Lauer, Johannes and Magdy, Amr and Nascimento, Mario and Ravada, Siva and Renz, Matthias and Sacharidis, Dimitris and Shahabi, Cyrus and Salim, Flora and Sarwat, Mohamed and Schoemans, Maxime and Speckmann, Bettina and Tanin, Egemen and Theodoridis, Yannis and Torp, Kristian and Trajcevski, Goce and van Kreveld, Marc and Wenk, Carola and Werner, Martin and Wong, Raymond and Wu, Song and Xu, Jianqiu and Youssef, Moustafa and Zeinalipour, Demetris and Zhang, Mengxuan and Zim\'{a}nyi, Esteban},
  title =	{{Mobility Data Science (Dagstuhl Seminar 22021)}},
  pages =	{1--34},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{12},
  number =	{1},
  editor =	{Mokbel, Mohamed and Sakr, Mahmoud and Xiong, Li and Z\"{u}fle, Andreas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.12.1.1},
  URN =		{urn:nbn:de:0030-drops-169190},
  doi =		{10.4230/DagRep.12.1.1},
  annote =	{Keywords: Spatio-temporal, Tracking, Privacy, Behavior, Data cleaning, Data management, Analytics}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.37
Tractability of Separation Logic with Inductive Definitions: Beyond Lists

Authors: Taolue Chen, Fu Song, and Zhilin Wu

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
In 2011, Cook et al. showed that the satisfiability and entailment can be checked in polynomial time for a fragment of separation logic that allows for reasoning about programs with pointers and linked lists. In this paper, we investigate whether the tractability results can be extended to more expressive fragments of separation logic that allow defining data structures beyond linked lists. To this end, we introduce separation logic with a simply-nonlinear compositional inductive predicate where source, destination, and static parameters are identified explicitly (SLID[snc]). We show that if the inductive predicate has more than one source (destination) parameter, the satisfiability problem for SLID[snc] becomes intractable in general. This is exemplified by an inductive predicate for doubly linked list segments. By contrast, if the inductive predicate has only one source (destination) parameter, the satisfiability and entailment problems for SLID[snc] are tractable. In particular, the tractability results hold for inductive predicates that define list segments with tail pointers and trees with one hole.
Cite as

Taolue Chen, Fu Song, and Zhilin Wu. Tractability of Separation Logic with Inductive Definitions: Beyond Lists. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.CONCUR.2017.37,
  author =	{Chen, Taolue and Song, Fu and Wu, Zhilin},
  title =	{{Tractability of Separation Logic with Inductive Definitions: Beyond Lists}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{37:1--37:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.37},
  URN =		{urn:nbn:de:0030-drops-77826},
  doi =		{10.4230/LIPIcs.CONCUR.2017.37},
  annote =	{Keywords: Separation logic, Inductive definitions, Satisfiability, Entailment}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.254
On the Satisfiability of Indexed Linear Temporal Logics

Authors: Taolue Chen, Fu Song, and Zhilin Wu

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
Indexed Linear Temporal Logics (ILTL) are an extension of standard Linear Temporal Logics (LTL) with quantifications over index variables which range over a set of process identifiers. ILTL has been widely used in specifying and verifying properties of parameterised systems, e.g., in parameterised model checking of concurrent processes. However there is still a lack of theoretical investigations on properties of ILTL, compared to the well-studied LTL. In this paper, we start to narrow this gap, focusing on the satisfiability problem, i.e., to decide whether a model exists for a given formula. This problem is in general undecidable. Various fragments of ILTL have been considered in the literature typically in parameterised model checking, e.g., ILTL formulae in prenex normal form, or containing only non-nested quantifiers, or admitting limited temporal operators. We carry out a thorough study on the decidability and complexity of the satisfiability problem for these fragments. Namely, for each fragment, we either show that it is undecidable, or otherwise provide tight complexity bounds.
Cite as

Taolue Chen, Fu Song, and Zhilin Wu. On the Satisfiability of Indexed Linear Temporal Logics. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 254-267, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.CONCUR.2015.254,
  author =	{Chen, Taolue and Song, Fu and Wu, Zhilin},
  title =	{{On the Satisfiability of Indexed Linear Temporal Logics}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{254--267},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.254},
  URN =		{urn:nbn:de:0030-drops-53767},
  doi =		{10.4230/LIPIcs.CONCUR.2015.254},
  annote =	{Keywords: Satisfiability, Indexed linear temporal logic, Parameterised systems}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.253
Extending Temporal Logics with Data Variable Quantifications

Authors: Fu Song and Zhilin Wu

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
Although data values are available in almost every computer system, reasoning about them is a challenging task due to the huge data size or even infinite data domains. Temporal logics are the well-known specification formalisms for reactive and concurrent systems. Various extensions of temporal logics have been proposed to reason about data values, mostly in the last decade. Among them, one natural idea is to extend temporal logics with variable quantifications ranging over an infinite data domain. In this paper, we focus on the variable extensions of two widely used temporal logics, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). Grumberg, Kupferman and Sheinvald recently investigated the extension of LTL with variable quantifications. They defined the extension as formulas in the prenex normal form, that is, all the variable quantifications precede the LTL formulas. Our goal in this paper is to do a relatively complete investigation on this topic. For this purpose, we define the extensions of LTL and CTL by allowing arbitrary nestings of variable quantifications, Boolean and temporal operators (the resulting logics are called respectively variable-LTL, in brief VLTL, and variable-CTL, in brief VCTL), and identify the decidability frontiers of both the satisfiability and model checking problem. In particular, we obtain the following results: 1) Existential variable quantifiers or one single universal quantifier in the beginning already entails undecidability for the satisfiability problem of both VLTL and VCTL, 2) If only existential path quantifiers are used in VCTL, then the satisfiability problem is decidable, no matter which variable quantifiers are available. 3) For VLTL formulas with one single universal variable quantifier in the beginning, if the occurrences of the non-parameterized atomic propositions are guarded by the positive occurrences of the quantified variable, then its satisfiability problem becomes decidable. Based on these results of the satisfiability problem, we deduce the (un)decidability results of the model checking problem.
Cite as

Fu Song and Zhilin Wu. Extending Temporal Logics with Data Variable Quantifications. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 253-265, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{song_et_al:LIPIcs.FSTTCS.2014.253,
  author =	{Song, Fu and Wu, Zhilin},
  title =	{{Extending Temporal Logics with Data Variable Quantifications}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{253--265},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.253},
  URN =		{urn:nbn:de:0030-drops-48475},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.253},
  annote =	{Keywords: Temporal logics with variable quantifications, satisfiability and model checking, alternating register automata, data automata}
}
  • Refine by Author
  • 3 Song, Fu
  • 3 Wu, Zhilin
  • 2 Chen, Taolue
  • 1 Almeida, Jussara
  • 1 Anderson, Taylor
  • Show More...

  • Refine by Classification
  • 1 Information systems → Data management systems
  • 1 Information systems → Information systems applications

  • Refine by Keyword
  • 2 Satisfiability
  • 1 Analytics
  • 1 Behavior
  • 1 Data cleaning
  • 1 Data management
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 1 2014
  • 1 2015
  • 1 2017
  • 1 2022

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