Regular Team Meeting

FLUENT Verification Project

Fri, 29 Jul 2022 10:36:51 -0600

Weekly Teleconference

Attending: Chris M, Zhen, Chris W, Mohammad, Lukas, Tom, Landon, Porter, Eric, Josh, Daniel, Andrew

Agenda

Workshop Discussion

Sessions for the workshop
Start time
- Thursday: 9am
- Friday: 8:30am?
Lynne McNeill confirmed she can join us

Updates from Students

Josh -- search improvements
Porter -- back in town; will try his method on C-element models in STORM
Landon -- helping with grant proposal; working on parallel path generator
Mohammad -- IWBDA abstract submitted
Chris W -- summarized progess and work assignments on the importance sampling simulator; nearing maturity
- Andrew: java software architect, organizing gradle build and class hierarchy.
- Tom: sparse model generator, acyclic constraint
- Daniel: constrain paths to terminate in multiple specified targets
- Eric: path distance constraint, any path reaching T should be not more than D distance from another path reaching T
Lukas -- progress on C-element model
Chris M on vacation next week

#meetings #workshop

meetings

Weekly Teleconference July 22, 2022

FLUENT Verification Project

Fri, 22 Jul 2022 10:53:53 -0600

Regular Team Meeting

Attending: Chris W, Chris M, Daniel, Tom, Mohammad, Lukas, Landon, Josh, Andrew,

Agenda

Added newer members to the Slack channel -- those not on Slack may be missing from the web site. Media to keep track of:
- Web site, mailing list, LEFT site, github
Scheduled fall meeting time: 4:30pm wednesdays (Mountain Time), 6:30 Eastern
Mohammad - IWBDA deadline pushed back, already written a 2pg abstract, needs title and short abstract.
Chris M -- cloud tool supplement, working on web frontend for simulation tools
Chris W -- brief overview of importance sampling on discrete spaces: we don't want to "enhance" transitions or reactions, we want to remove unfruitful paths while leaving everything else alone. Judicious rate zeroing should be the way to approach an optimal sampling distribution.
Josh -- summarized software work, some issues with conversions
Landon -- parallel path generation is working better than anticipated; showed a result for the yeast polarization model
Workshop sessions:
- STAMINA
- Importance sampling
- Azure deployment
- Continuing to curate examples
- How to apply our approaches to genetic circuits
- Planning sessions
- Education, online course planning
Some sessions could be discussion while others are "hacking" sessions
Will work on a flyer to advertise the outreach event; may rope in faculty from other departments, e.g. digital folklore, anthropology

#meetings

meetings

Weekly Teleconference July 8, 2022

FLUENT Verification Project

Fri, 08 Jul 2022 10:31:04 -0600 last edited: Fri, 08 Jul 2022 10:59:45 -0600

Regular Team Meeting

Attending: Chris W, Chris M, Zhen, Tom, Eric, Daniel, Mohammad, Andrew, Josh, Lukas, Hao

Agenda

Mohammad -- working to derive confidence intervals for existing data and results so that new experiments are not needed. Running another simulation with a less rare property. Would like everyone to look over responses in the paper. The other paper (IWBDA abstract) is not done; will be a two-page abstract.
Chris M -- got supplemental support for a cloud server to host software products
Chris W -- undergrads are continuing to work on importance sampling simulation tool; workshop web site and video are now live, with registration form. #^Outreach Event - FLUENT
Zhen -- working on proposal, no meetings next week.
Josh -- worked on async multithreading for STAMINA. Trying to improve performance on two-inverter circuit.
Porter -- going on a work trip with SDL to Indiana (not India).
Andrew -- described pull requests for code updates in the usu_importance_sampling repo
Eric, Daniel -- going through tutorials on Importance Sampling

Research Workshop Plans.

Breakout group topics(?)

Brainstorm topics with respective groups
Survey of genetic circuit applications; Chris M could reprise his tutorial on genetic circuits.
Start a Google Doc or Sheet to setup schedule

Everyone needs to book travel. Hampton Inn and Marriott are recommended hotels in the area. Chris M planning to stay in Logan on Thursday night.

#meetings

meetings

Weekly Teleconference July 1, 2022

FLUENT Verification Project

Fri, 01 Jul 2022 10:33:29 -0600

Regular Team Meeting

Attending: Hao, Zhen, Chris W, Josh, Lukas, Mohammad, Andrew, Daniel, Eric, Landon, Porter, Tom

Agenda

Zhen: Making progress on outreach event, making advertising materials (video, flyer, web site), working with university advisors in exploratory majors to advertise to students who might be inclined to shift majors into computing-related fields. Workshop split across three days with themes: "Treading in a Sea of Data", "Everything is Computing", and "Trustworthy Computing".
- Josh web page demo with cycling ocean video, will use as advertisement. Page also has registration form. Registration form data should be added to a database on the left server.

#meetings #outreach

meetings

Weekly Meeting Dec 4, 2020

Winstead

Fri, 04 Dec 2020 16:34:12 -0700

!FLUENT Verification Project

Regular Teleconference

Attending: Hao, Riley, Zhen, Chris W, Porter, Mohammad, Lukas, Nisa, Tom, Payton, Laureano

Agenda

Hao and Mohammad -- has been changing the code base entirely so that we can expand counterexample graph not from patterns but from transitions. New version doesn't work for PRISM models yet but is working for some abstract models. Discussion on importance sampling and stochastic simulation -- IS needs to be specialized to a particular type of property. Some discussion on Gillespie's algorithm and relationship between biochemical systems and CTMC models.
Laureano -- update on IC3, better understanding of the basic structure.
Nisa -- working on documenting code, cleaning up folder and file organization.
Chris W & Tom -- developing a simple model of a faulty asynchronous data interface in PRISM, will use it along with Hao/Mohammad's counterexample model to explore IS options. Will post some papers on IS in CTMC.
Zhen & Riley -- Update on Hazard Analysis iBiosim & STAMINA paper. Having some crashes due to insufficient memory.
Lukas -- still working on paper; Riley will be second author.
Porter -- working on various details.

#meetings

meetings

Winstead

Fri, 04 Dec 2020 16:54:33 -0700

I've uploaded some papers that are relevant to importance sampling on Markov models. An important application is Mean Time to Fail (MTTF), which is close to the type of problems we are studying. I've added some of the papers to the Zotero folder on Importance Sampling, and you can access the pdf documents here:

https://left.engr.usu.edu/cloud/winstead/Importance_Sampling_Papers

Some good places to start are:
* Importance Splitting paper
* MTTF Estimation paper

Weekly Meeting Nov 13, 2020

Winstead

Fri, 13 Nov 2020 16:18:01 -0700

!FLUENT Verification Project

Regular Teleconference

Attending: Chris W, Tom, Mohammad, Chris M, Nisa, Lukas, Laureano, Riley, Zhen, Hao,

Agenda

Zhen -- can deprecate average state resident time in favor of Riley's estimate method.
Lukas -- finished midterms; learning iBiosim CLI; improving illustration skills. Some discussion of redoing simulations on deep learning machine, but may take too long. For the paper, could use a moderate number of runs on a personal machine to get some data sooner. For runtime comparisons, Chris M is concerned that all results should be reported from the same machine.
Hao -- Some surprise that another tool (DiPro) is running faster than our code; working on some optimizations. It's good to have a benchmark for comparison. DiPro is in Java, connected to PRISM. There are a number of places where Mohammad's code can be optimized.
Nisa -- expecting to deliver some content soon, will add information to readme; Nisa will focus on coursework during the spring semester
Laureano -- did some pseudocode this week, will be translating from pseudocode to a test implementation
Chris W -- working with tom, working on async stochastic paper, should appear in the github repository

#meetings

meetings

Weekly Meeting Aug 29, 2020

Winstead

Fri, 30 Oct 2020 16:30:59 -0600

!FLUENT Verification Project

Attending: Chris W, Zhen, Lukas, Tom, Laureano, Mohammad, Nisa, Payton, Riley

Agenda

Chris W -- making progress with Tom, moving onto MC integration for state machines and Markov models. Zhen will try and recruit another REU student since Darren is out this semester. Chris W will see if Darren is interested in rejoining during spring.
Lukas is working on a paper; will get contributions from Zhen and Riley
Payton -- status of reb2sac in docker looks promising, not done yet. Java code is Dockerized.
Mohammad -- fixed a bug that shows wrong probabilities in subgraphs
Nisa -- running new models with bounded model checking on DTMC, moving code around
Laureano -- almost ready to implement IC3, still studying T3
Riley -- Doing heuristic exploration to iteratively change reachability rather than recursively. Starts with a kappa of 1, then divides kappa by 2 in subsequent iterations. Similar to parametric optimization frameworks? Homotopy methods?

#meetings

meetings

Winstead

Fri, 30 Oct 2020 16:37:32 -0600

@Riley Roberts what you're doing probably fits into a subclass of iterative methods, of which there are many. A particularly exotic example is the homotopy method, which takes a hard problem and "distorts" it into an easy problem. Then, by small increments, the easy problem is deformed back into the hard problem in such a way that each incremental step converges when using information from the previous step.

Zhen Zhang

Fri, 30 Oct 2020 20:56:48 -0600

@Winstead Thanks, Chris. I asked Riley to formulate an algorithm for the improvement he made. I think it will help us to see more clearly on how it fits the homotopy method.

Weekly Meeting Oct 23, 2020

Winstead

Fri, 30 Oct 2020 15:27:18 -0600

!FLUENT Verification Project

Regular Team Meeting

Attending: Chris W, Payton, Tom, Riley, Porter, Nisa, Mohammad, Laureano, Lukas, Chris M

Agenda

Chris W -- working with Tom on MC integration; need to learn how to implement sample weighting in PRISM. Can this be done in API? Need to investigate "tight integration" with PRISM.
Hao and Mohammad -- trying to figure out inconsistency in subgraph probability. Something is wrong when there are loops in the subgraph. Only a few bugs left. Nisa is making progress on the solver, a basic interface is in place. Laureano still studying IC3 paper.
Payton -- containerized core functionality of iBioSim. Within a few days there should be online access. Compiling reb2sac (C) within a Docker container is challenging.
Lukas -- updated models, working with Riley to translate un/bounded versions. Working on a paper.
Riley -- wrote script with Lukas, now on GitHub. Recent code changes and cleaning opened room for optimizations. Made five or six little optimizations that cumulatively boosted speed.
Porter -- working on a new way of modeling toggle switch, calculating repression/degradation probabilities. New method appears to have less variance, but the convergence is erratic. Shouldn't it be smooth?

#meetings

meetings

Weekly Meeting Oct 9, 2020

Winstead

Mon, 12 Oct 2020 10:10:34 -0600

!FLUENT Verification Project

Regular Team Meeting

Attending: Hao, Chris W, Zhen, Lukas, Tom, Payton, Laureano, Nisa, Mohammad, Riley

Agenda

Lukas: Got new computer. New updates are confirmed. Rileys changes give same results. Zhen recommends using remote access to free up Lukas' resources.
Riley: pushed STAMINA update to fix issues from last week, also pushed some efficiency boosters. Was able to resolve incomplete cases that previously failed to converge. Now converge to narrow range in 3 hours. Other cases converges in as little as 6 minutes. Can get narrow bound with much fewer states, less memory needed.
Payton- still working on Dockerization of iBioSim
Nisa: reorganizing, "flattening" model code. The modified model doesn't work exactly the same as the original.
Laureano: learning basics on a IC3 SAT solver, which is a sophisticated platform.

#meetings !FLUENT Verification Project

meetings

Weekly Meeting Oct 2, 2020

Winstead

Fri, 02 Oct 2020 16:31:26 -0600

!FLUENT Verification Project

Regular Team Meeting

Attending: Laureano, Lukas, Hao, Mohammad, Nisa, Porter, Riley, Tom, Zhen, Chris W, Chris M

Agenda

Recounted good things from the week, to start on a positive note.
Zhen -- Riley found several issues in STAMINA
- None of them make results wrong, just efficiency issues
- In a given exploration of a state, it returned multiple transitions to the same state. Parallel transitions override probability rather than summing. Not clear why parallel transitions are occurring. Not every transition has parallels. Is it due to bounding, i.e. we're retaining the most probable transition? Uniformized CTMCs should zero out "dummy" transitions. Can we try a uniformized model and see if the bug still happens? Maybe use PRISM to uniformize, then run the uniformized model back through STAMINA?
- Porter: showed two different degradation and repression models, the "old one" (linear), and a "new one". Seeing some glitch or numerical format issue with probability results.
Hao: Mohammad debugged a major issue
- Solved a spurious looping problem, and implemented a version of the subgraph analysis (as opposed to sets of paths). Tried for models up to 70k states. Speedup is apparent in test cases.
- Nisa: fixed calculation problem, started working on new model. Working on more sophisticated DTMC model.
- Laureano: Looking for case examples for MTBDD analysis.
Chris W: working with Tom on MC integration. Mohammad suggests looking at the PLASMA Lab tool which does importance samplding and uses PRISM/
Chris M: Payton has got iBioSim dockerized to make it more portable. Need to give him some modeling tasks.

Announcements

Chris M will be working on the COMBINE event next week. COMBINE is running from Sunday evening through the week. Registration is free and may be of interest members of this group.
Hao will run the meeting next week.

#meetings

meetings

Weekly Meeting Sept 18, 2020

Winstead

Fri, 18 Sep 2020 16:31:45 -0600

!FLUENT Verification Project

Regular Team Meeting

Attending: Chris M, Hao, Chris W, Tom, Riley, Lukas, Mohammad, Nisa, Zhen

Riley: was including absorbing state in Pmin calculation. Removed from the loop, seems to have fixed the issue. Now moving onto some other edge cases. Changes are pushed to GitHub.
Porter: new method is not doing so well. Regarding discrepancies, Zhen: "Which one is the ground truth?" Chris M: "They should agree at 100. Why don't they?" Also discussed other discrepancies.
Tom: Studying MC simulation models
Chris W: re-starting the engine on importance sampling, going to revisit Hao and Mohammad's model from the hack session. Looking at the paper on "neural bridge sampling", will report back on if it's worth discussing with the whole group.
Hao, Mohammad: managing memory consumption related to path prefix and suffix. Discussion of representation of states vs paths.

#meetings

meetings

Weekly Meeting Sept 11, 2020

Winstead

Fri, 11 Sep 2020 16:35:48 -0600

!FLUENT Verification Project

Regular Team Meeting

Attending:Chris M, Tom, Riley, Zhen, Curtis, Laureano, Lukas, Chris W, Mohammad, Nisa, Payton, Pedro, Hao

Agenda

Riley described an error in STAMINA that fails to reproduce results from iBioSim. The cause of the error is not yet known. There is a range of kappas where the probability bound expands before shrinking; it should shrink monotonically. Chris M: "Don't play loose with your equal signs."
Mohammad: described a subgraph growth algorithm, calculating probability of combined subgraphs. If a specified bound is passed, the subgraph is returned as a counterexample.
Nisa: using SAT solver

#meetings

meetings

Weekly Meeting Aug 14, 2020

Winstead

Fri, 14 Aug 2020 12:55:04 -0600

!FLUENT Verification Project

Regular Team Meeting

Attending: Chris M, Curtis, Chris W, Laureano, Lukas, Mohammad, Nisa, Payton, Tom, Zhen, Hao

Agenda

Importance sampling tutorials: Shared links to make sure everyone can access them. Can find tutorials on LEFT site using a keyword search: https://left.engr.usu.edu/search?tag=tutorials
Discussion of stochastic simulation, stochastic PDEs and chemical Langevin equation (CLE).
New international grad student problems are not resolved. Spring arrival may not be realistic.
Recruiting undergrads is probably necessary, need to be proactive and advertise grad school opportunities, inform students about the process, funding, etc.
NSF Annual Report approved
Zhen gave a progress update. Discussed buggy STAMINA results with "Probability 1" failure, it doesn't make sense that all paths fail before reaching an absorbing state.
Lukas' IWBDA paper is being developed into a journal article draft.
Hao and Mohammad -- fully integrated cex generation with PRISM, seeing some performance problems that need to be fixed. Nisa is looking at Z3 solver. Laureano is studying PRISM source.
Chris W -- looking at some existing tutorials on Monte Carlo methods, will share with the group if we find a good one.
Lukas moved to Boulder. Found some model mistakes in the modified hazard circuit.
Payton is getting help from Jonathon Kerr
No meeting next week, subsequent meetings will be at 3:30pm.

#meetings

meetings

Weekly Meeting Aug 7, 2020

Winstead

41.7468 -111.8268, Fri, 07 Aug 2020 11:06:38 -0600

!FLUENT Verification Project

Regular Team Meeting

Attending: Chris W, Hao, Zhen, Trent, Lukas, Nisa, Laureano, Payton, Mohammad,

Agenda

Discussion on importance sampling and Monte Carlo

Discussion of IWBDA -- interesting paper on Monte Carlo simulation of genetic circuits. Zhen joined some short talk sessions.

Zhen pointed us to the SubSBML project: https://github.com/BuildACell/subsbml

Sub-SBML is a Python based toolbox to create, edit, combine, and model interactions among multiple Systems Biology Markup Language (SBML) models. Sub-SBML works with a “subsystem” architecture of modeling where a single SBML model can be contained within a subsystem. Three major functionalities are developed in Sub-SBML that take advantage of this subsystem framework of modeling –
creating subsystems, combining multiple subsystems, and modeling interactions such as transport of molecules and input-output relationships among multiple subsystems.

Payton -- discussed about how SBOL models do not have unique mappings to SBML.

Lukas: Can you annotate SBOL with SBML?

Erik Winfree's group requested a tutorial on iBioSim.

Python library to make genetic circuit figures DNAplotlib https://github.com/VoigtLab/dnaplotlib

Trent is joining Sarcos, this is his last day. Zhen will take over his code, most likely will be carried forward by Riley in the fall.

#meetings

meetings

Chris Myers

Sun, 09 Aug 2020 19:34:34 -0600

You can connect SBOL to SBML via the Model Class. You can annotate SBML with SBOL URIs too (see Roehner's ACS SynBio paper on this subject).

I think it is Richard Murray's group that reached out to us.

Weekly meeting July 24, 2020

Winstead

Fri, 24 Jul 2020 10:58:21 -0600

!FLUENT Verification Project

Regular Teleconference

Attending: Chris M, Hao, Mohammad, Lukas, Tom, Payton, Laureano, Nisa, Curtis, Chris W

Announcements

IWBDA virtual conference coming up, everyone should attend. #^https://www.iwbdaconf.org/2020/
Chris M unavailable for a couple of weeks.
Next Friday will be discussion session on Importance Sampling tutorial. The video and slides will be posted ahead of time.
NSF annual report draft should be finalized on Monday
Everyone should fill in the when2meet poll: #^https://www.when2meet.com/?9412880-ptDIQ

Agenda

Hao, Mohammad, Laureano, Nisa -- progress update, still need full integration with PRISM
Chris W, Tom -- returning from "vacation", working on importance sampling tutorial
Chris M, Lukas, Payton -- working on IWBDA abstract and presentation

#meetings

meetings

Weekly Teleconference June 26, 2020

Winstead

Fri, 26 Jun 2020 11:29:05 -0600

!FLUENT Verification Project

# Regular Team Meeting

Attending: Chris M, Hao, Lukas, Trent, Mohammad, Tom, Payton, Laureano, Nisa, Zhen, Chris W

## Agenda

* Chris M
   * Lukas — new case studies, networks with known function hazards. Will do analysis to determine best topology.
   * Another interesting Beal paper on SNR of circuits, now on Zotero, “Signal-to-Noise Ratio Measures Efficacy of Biological Computing Devices and Circuits.”
   * Payton — trying to build a command wrapper around iBioSim analysis tool.
* Chris W — importance sampling discussion, document available on github in “paper_drafts” repository.
* Hao
   * Mohammad — algorithms for finding paths in bounded-until formulas; counterexample meeting with Zhen’s group. Clarification: we want to find counter examples on the truncated state space. Might be interesting to know what kind of paths end in the absorbing state.
   * Nisa — going through code, starting to get it
   * Laureano — studying PRISM code
* Zhen — Porter started internship on Wednesday.  Comparing with related tool from recent CAV tool paper. Will share the paper on Zotero.
   * Trent — early termination problem

**No meeting next week, 4th of July holiday.** Meet again in two weeks.

**Chris W will record a tutorial on importance sampling, should be ready in about two weeks**. Will notify group when it’s ready, and we’ll watch in advance then do a Q&A at the teleconference meeting.

#meetings

Meetings

Weekly Teleconference June 19, 2020

Winstead

Fri, 19 Jun 2020 11:42:45 -0600 last edited: Fri, 19 Jun 2020 11:47:25 -0600

!FLUENT Verification Project

Regular Team Meeting

Attending: Chris M, Chris W, Zhen, Hao, Trent, Tom, Mohammad, Laureano, Lukas, Payton, Nina, Porter, Curtis

Agenda

Zhen updates
- Trent — trying to run STAMINA on toggle switch with different kappa values. Multi-iterations differ from single-run results. State spaces differ, with different perimeter states.
- Porter — question on JETC paper toggle switch model. PRISM model behavior changes significantly with minor changes in parameters. Curtis worked on the model. Memory fog obscures the answer. TetR has a narrower range than LacI because the property is satisfied for higher values of TetR. LacI starts at 60, with 9 levels between 0 and 80. TetR has 11 levels between 0 and 50. LacI changes by 10, TetR changes by 5. Model is in github repository under Critical-Values-Prototype .
Hao — working on bounded until formulas
- Mohammad — we do find counter-examples for bounded-until properties, but returns very large sets. Discussion on tool integration.
Chris W — working on importance sampling on a benchmark model
Chris M — some work on genetic circuit hazards, using stochastic analysis to “score” different design choices that one might make. Lukas working on a paper on this topic. Lukas also working on a phage lambda model. Interesting paper on extrinsic vs instrinsic noise, Lukas will upload to Zotero. Extrinsic noise changes gamma-distributed responses to lognormal-distributed responses. Title: Biochemical complexity drives log-normal variation in genetic expression.

#meetings

!fluent@left.engr.usu.edu Meetings

Workshop Tutorial Day: Jun 5, 2020

Winstead

Fri, 05 Jun 2020 13:58:18 -0600

!FLUENT Verification Project

Virtual workshop started at 10AM ET.

Attending: Chris M, Zhen, Hao, Chris W, Lukas, Pedro, Nisa, Trent, Laureano, Payton, Tom, Porter, Mohammad,

Tutorials:

Chris W: Measure Theory
Zhen: Probabilistic Model Checking
Hao: Bounded Model Checking
Chris M: Formal Verification in Synthetic Biology

Slides to be posted on this site and also on Zotero.

#tutorials #workshop #meetings #ModelChecking #MeasureTheory #BoundedModelChecking

meetings workshop

show all 4 comments

Zhen Zhang

Sun, 07 Jun 2020 11:04:47 -0600

Hi @Winstead. I kept getting the following error when opening your tutorial PDF: The file “Measure Theory Tutorial.pdf” could not be opened because it is empty.

Winstead

Mon, 08 Jun 2020 14:11:11 -0600

This link should work: Measure Theory Tutorial

Zhen Zhang

Mon, 08 Jun 2020 14:14:23 -0600

Thanks. Yes, I was able to download them.

Weekly meeting May 29, 2020

Winstead

Fri, 29 May 2020 11:41:29 -0600

!FLUENT Verification Project

Regular Teleconference

Attending: Chris M, Lukas, Trent, Nisa, Chris W, Mohammad, Zhen, Porter, Payton, Curtis, Tom, Laureano, Hao

Agenda

Lukas: Discrepancy in STAMINA results, Zhen suggested an explanation. Probably due to software version.
Chris W: can provide SSH tunnel accounts via left.engr.usu.edu
Porter: discussion of "glitch" meaning
Chris W:
- homework assignment on basic set theory, as preparation for the tutorial (attached to this post)
- demos will be shared using Matlab Online, #^https://matlab.mathworks.com
Workshop planning

#meetings

meetings

Weekly meeting

Winstead

Fri, 22 May 2020 11:40:20 -0600

!FLUENT Verification Project
I forgot to put this on the forum page. Reposting from my channel.

Regular Teleconference

Attending: Chris W, Chris M, Zhen, Tom, Porter, Trent, Mohammad, Payton, Lukas, Nisa, Laureano, Hao

Agenda

Planning for the workshop meeting
- Tutorials:
  - Chris W
  - Zhen
  - Importance Sampling? (Could do IS in one of the weekly meetings)
- Need to plan hacking sessions and organize discussion topics.
Zhen: started working with models from Lukas, found a discrepancy between model checking and iBiosim results. Needed to correct inequalities in properties.
Hao: just had summer kickoff meeting with Nisa and Laureano. Mohammad finished search algorithms.
- Mohammad: integration issue is somewhat resolved, can pass expressions now, but not properties. Only thing left is to get the expreession inside the property. It's almost 100% automated now.
Problems with travel and international students. Can we put them on the payroll? Can we enroll them remotely?

meetings